blob: 29686a26c131dcde7364f015dccc3774b6754ee0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Fixpoint demo_recursion(n:nat) := match n with
|0 => Type
|S k => (demo_recursion k) -> Type
end.
Record Demonstration := mkDemo
{
demo_law : forall n:nat, demo_recursion n;
demo_stuff : forall n:nat, forall q:(fix demo_recursion (n : nat) : Type :=
match n with
| 0 => Type
| S k => demo_recursion k -> Type
end) n, (demo_law (S n)) q
}.
Theorem DemoError : Demonstration.
Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*)
|
