blob: 831e8fb507a1c0a45d2e1fb5ffbeba63a9b15973 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Fixpoint arrow (n: nat) :=
match n with
| S n => bool -> arrow n
| O => bool
end.
Fixpoint apply (n : nat) : arrow n -> bool :=
match n return arrow n -> bool with
| S n => fun f => apply _ (f true)
| O => fun x => x
end.
Axiom f : arrow 10000.
Definition v : bool := Eval compute in apply _ f.
Definition w : bool := Eval vm_compute in v.
|
