Quelle bug_11766.v Sprache: Coq

Require Import Program.Tactics.

Set Universe Polymorphism.

Module Bug11766.

Program Definition bla@{} : nat := _.
Next Obligation.
  let x := constr:(Type) in exact 0.
Defined. (* was unbound univ *)

Program Definition bla'@{} : nat := _.
Solve Obligations with let x := constr:(Type) in exact 0. (* was unbound univ *)

End Bug11766.

From Corelib Require Import ssreflect.

Module Bug11988.

#[local]
Obligation Tactic := idtac.

Section Foo.

Universe u.

Variable T : Type@{u}.
Variable op : T -> T -> T.
Hypothesis opC : forall x y, op x y = op y x.

Program Definition foo@{} x y : {z : T & z = op x y} :=
  existT _ (op y x) _.

Next Obligation.
move=> /= x y.
by rewrite -[RHS]opC.
Qed. (* should work even though rewrite [RHS] adds a spurious universe *)

End Foo.

End Bug11988.

Module ExampleFrom11902.

Local Unset Universe Polymorphism.

Program Definition foo (X : Type) : Type :=
  let x := X in forall x : x, _.

Next Obligation.
refine nat.
Defined.

End ExampleFrom11902.

quality99%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

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.