Defined constructors enhancements

[valis]

We can define the type of vectors as the following record:

\record Vec (A : \Type) (n : Nat) (list : List A) (proof : length list = n)

The problem is that we cannot define functions over it by pattern matching with vnil and vcons as usual. We could try to define them as new constructors:

\cons vnil {A : \Type} => \new Vec A 0 nil idp

\cons vcons {A : \Type} {n : Nat} (a : A) (v : Vec A n) : Vec A (suc n) \elim v
  | (xs,p) => \new Vec A (suc n) (cons a xs) (pmap suc p)

To do this, we need to implement the following enhancements:

• [ ] Allow arbitrary expressions in implementations of properties in RHS (as pmap suc p in the example above).
• [ ] Allow constructors defined by pattern matching (as vcons).
• [ ] Variables in implementations of properties in LHS may not occur in RHS or occur only in implementations of properties (as p in vcons). It is impossible to recover them in general. Thus, the user should provide a function which does that. It can also be generated by a meta when possible.

[ice1000]

Allow constructors defined by pattern matching (as vcons).

Maybe #142

[valis]

This is a generalization of #187.