Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_3217.v Sprache: Coq

Original von: Coq^©

(** [Set Implicit Arguments] causes Coq to run out of memory on [Qed] before c3feef4ed5dec126f1144dec91eee9c0f0522a94 *)
Set Implicit Arguments.

Variable LEM: forall P : Prop, sumbool P (P -> False).

Definition pmap := option (nat -> option nat).

Definition pmplus (oha ohb: pmap) : pmap :=
match oha, ohb with
| Some ha, Some hb =>
   if LEM (oha = ohb) then None else None
| _, _ => None
end.

Definition pmemp: pmap := Some (fun _ => None).

Lemma foo:
True ->
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
    (pmplus pmemp
     pmemp))))))))))))
    =
    None -> True.
Proof.
  auto.
Timeout 2 Qed.

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.