blob: e07fdcf8314825e3bbec57ef854f9c543d98e281 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Sections taking care of let-ins for inductive types *)
Section Foo.
Inductive foo (A : Type) (x : A) (y := x) (y : A) := Foo.
End Foo.
Section Foo2.
Variable B : Type.
Variable b : B.
Let c := b.
Inductive foo2 (A : Type) (x : A) (y := x) (y : A) := Foo2 : c=c -> foo2 A x y.
End Foo2.
|
