Quelle bug_15554.v Sprache: Coq

Set Primitive Projections.
Record Box {T} := box { unbox : T }.
Arguments Box : clear implicits.
Definition indirect := @unbox.
Goal forall T : @Box Set, unbox T -> False.
  intros T x.
  let Tindirect := constr:(indirect _ T) in
  let Tdefined := eval cbv [indirect] in Tindirect in
  let Tfolded := type of x in
  cbv [unbox] in x;
  let Tunfolded := type of x in
  match Tdefined with Tdefined => idtac end;
  match Tfolded with Tfolded => idtac end;
  match Tfolded with Tunfolded => idtac end;
  match Tdefined with Tfolded => idtac end;
  match Tdefined with Tunfolded => idtac end;
  match Tfolded with Tdefined => idtac end;
  (* matches above have passed for a while
     matches below used to fail with "Error: No matching clauses for match." *)
  match Tunfolded with Tunfolded => idtac end;
  match Tunfolded with Tfolded => idtac end;
  match Tunfolded with Tdefined => idtac end;
  assert_fails (constr_eq Tdefined Tfolded);
  assert_fails (constr_eq Tdefined Tunfolded);
  assert_fails (constr_eq Tfolded Tunfolded);
  idtac Tdefined Tfolded Tunfolded.
Abort.

quality100%

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