Quelle bug_2017.v Sprache: Coq

(* 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.

Parameter choose : forall(P : bool -> Prop)(H : exists x, P x), bool.

Parameter H : exists x : bool, True.

Definition coef :=
match Some true with
  Some _ => @choose _ H |_ => true
end .

quality99%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.