Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: hyps_inclusion.v Sprache: Coq

Original von: Coq^©

(* Simplified example for bug #1325 *)

(* Explanation: the proof engine see section variables as goal
   variables; especially, it can change their types so that, at
   type-checking, the section variables are not recognized
   (Typeops.check_hyps_inclusion raises "types do no match").  It
   worked before the introduction of polymorphic inductive types because
   tactics were using Typing.type_of and not Typeops.typing; the former
   was not checking hyps inclusion so that the discrepancy in the types
   of section variables seen as goal variables was not a problem (at the
   end, when the proof is completed, the section variable recovers its
   original type and all is correct for Typeops) *)

Section A.
Variable H:not True.
Lemma f:nat->nat. destruct H. exact I. Defined.
Goal f 0=f 1.
red in H.
(* next tactic was failing wrt bug #1325 because type-checking the goal
   detected a syntactically different type for the section variable H *)
case 0.
Abort.
End A.

(* Variant with polymorphic inductive types for bug #1325 *)

Section B.
Variable H:not True.
Inductive I (n:nat) : Type := C : H=H -> I n.
Goal I 0.
red in H.
case 0.
Abort.
End B.

¤ Dauer der Verarbeitung: 0.15 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.