Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Template.v Sprache: Coq

Original von: Coq^©

(*
Module TestUnsetTemplateCheck.
  Unset Template Check.

  Section Foo.

    Context (A : Type).

    Definition cstr := nat : ltac:(let ty := type of A in exact ty).

    Inductive myind :=
    | cons : A -> myind.
  End Foo.

  (* Can only succeed if no template check is performed *)
  Check myind True : Prop.

  Print Assumptions myind.
  (*
  Axioms:
  myind is template polymorphic on all its universe parameters.
   *)
  About myind.
(*
myind : Type@{Top.60} -> Type@{Top.60}

myind is assumed template universe polymorphic on Top.60
Argument scope is [type_scope]
Expands to: Inductive Top.TestUnsetTemplateCheck.myind
*)
End TestUnsetTemplateCheck.
*)

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