1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Some check about implicit arguments in fix *)
Check fix f {f:nat} := match f with 0 => true | _ => false end.
CoInductive stream := { this : nat ; next : option stream }.
Check cofix f {f:nat} := {| this := f ; next := None |}.
(* The following was ok from 8.4, just checking that the order is not
mixed up accidentally *)
Check fix f (x : nat) (x : forall {a:nat}, a = 0 -> nat) :=
match x eq_refl with 0 => true | _ => false end.
Check fix f (x : forall {a:nat}, a = 0 -> bool) (x : nat) :=
match x with 0 => true | _ => false end.
|
