Quellcode-Bibliothek bug_7443.v Sprache: Coq

Inductive type := nat | bool.
Definition denote (t : type)
  := match t with
     | nat => Datatypes.nat
     | bool => Datatypes.bool
     end.
Ltac reify t :=
  lazymatch eval cbv beta in t with
  | Datatypes.nat => nat
  | Datatypes.bool => bool
  end.
Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
Axiom Literal : forall {t}, denote t -> Type.
Declare Scope foo_scope.
Delimit Scope foo_scope with foo.
Open Scope foo_scope.
Section A.
  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
  Check [1]. (* Literal 1 : Type *) (* as expected *)
  Notation "[ x ]" := (Literal x) : foo_scope.
  Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *)
  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
  Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable:
  #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *)
End A.
Section B.
  Notation "[ x ]" := (Literal x) : foo_scope.
  Check @Literal nat 1. (* [1] : Type *)
  Fail Check [1]. (* As expected: The command has indeed failed with message:
  The term "1" has type "Datatypes.nat" while it is expected to have type
   "denote ?t". *)
  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
  Check [1]. (* Should succeed, but instead fails with: Error:
  The term "1" has type "Datatypes.nat" while it is expected to have type
  "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *)
End B.

quality99%

¤ 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.0.7Bemerkung: ¤

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.