1
(* Cases with let-in in constructors types *)
4
k : let x := t in x -> x.
8
(* Do not contract nested patterns with dependent return type *)
13
Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
14
match eq_nat_dec x y return P y with
16
match eqprf in (_ = z) return (P z) with
24
(* Use notations even below aliases *)
28
Fixpoint foo (A:Type) (l:list A) : option A :=
31
| x0 :: nil => Some x0
32
| x0 :: (x1 :: xs) as l0 => foo A l0
37
(* Do not duplicate the matched term *)
39
Axiom A : nat -> bool.