|
(* Checking typability of intermediate return predicates in nested pattern-matching *)
Inductive A : (Type->Type) -> Type := J : A (fun x => x).
Definition ret (x : nat * A (fun x => x))
:= match x return Type with
| (y,z) => match z in A f return f Type with
| J => bool
end
end.
Definition foo : forall x, ret x.
Proof.
Fail refine (fun x
=> match x return ret x with
| (y,J) => true
end
).
Abort.
¤ Dauer der Verarbeitung: 0.16 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.
|
