blob: 61f89d403ae9d14ab4324eeed8b8079b979197f3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
(* Cases with let-in in constructors types *)
Inductive t : Set :=
k : let x := t in x -> x.
Print t_rect.
(* Do not contract nested patterns with dependent return type *)
(* see bug #1699 *)
Require Import Arith.
Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
match eq_nat_dec x y return P y with
| left eqprf =>
match eqprf in (_ = z) return (P z) with
| refl_equal => def
end
| _ => prf
end.
Print proj.
(* Use notations even below aliases *)
Require Import List.
Fixpoint foo (A:Type) (l:list A) : option A :=
match l with
| nil => None
| x0 :: nil => Some x0
| x0 :: (x1 :: xs) as l0 => foo A l0
end.
Print foo.
|
