Quelle bug_17868.v Sprache: Coq

From Corelib Require Import PrimInt63 PrimArray.

Class pointed T := point : T.

Inductive PROOF_OF A := the (x : A).

Definition foo : PROOF_OF (@make (pointed nat) 0 0 = @make nat 0 0).
  constructor.
  cbv. (* @eq (array@{pointed.u0} nat) [| | O : nat |]@{pointed.u0} [| | O : nat |]@{Set} *)
  reflexivity.
Defined.

Notation barv
  := (@exist (array@{Set} nat) (fun x => x = @make nat 0 0) _ (eq_refl (@make nat 0 0)))
       (only parsing).

Definition bar1 : { x | x = @make (pointed nat) 0 0 }
  := Eval cbv in barv.

Definition bar0 : { x | x = @make (pointed nat) 0 0 }
  := Eval vm_compute in barv.

Definition bar := Eval cbv in foo.

quality99%

¤ 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.