|
(* Some check of Miller's pattern inference - used to fail in 8.2 due
first to the presence of aliases, secondly due to the absence of
restriction of the potential interesting variables to the subset of
variables effectively occurring in the term to instantiate *)
Set Implicit Arguments.
Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
Variable H : exists x : bool, True.
Definition coef :=
match Some true with
Some _ => @choose _ H |_ => true
end .
¤ 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.
|
