|
(* 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.
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
