Getting usable constructors from an inductive type.

Stream: lean4

[ohhaimark]

Say I have the following inductive datatype

inductive Vec : Type → Nat → Type where
  | nil : Vec a 0
  | cons : a → Vec a n → Vec a (n+1)

how can I, from say CommandElabM, get a list of constructors whose return type unifies with Vec a n for some a n.

For example Vec Nat 0 can't unify with Vec a (n+1), so using cons is impossible. I believe lean should already do this internally for exhaustiveness checking.

Ultimately I want to calculate the number of bits to encode an inductive datatype, but a naive approach doesn't account for dependent inductive types, i.e Vec Bool 3 requires more bits then Bool × Bool × Bool when done naively.