blob: bb673f38c236372ea2e090782edfe17148267d4a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* Test support of let-in in arity of inductive types *)
Inductive Foo : let X := Set in X :=
| I : Foo.
Definition foo (x : Foo) : bool :=
match x with
I => true
end.
Definition foo' (x : Foo) : x = x.
case x.
match goal with |- I = I => idtac end. (* check form of the goal *)
Undo 2.
elim x.
match goal with |- I = I => idtac end. (* check form of the goal *)
Undo 2.
induction x.
match goal with |- I = I => idtac end. (* check form of the goal *)
Undo 2.
destruct x.
match goal with |- I = I => idtac end. (* check form of the goal *)
|
