Quelle PrintInfos.v Sprache: Coq

(* coq-prog-args: ("-top" "PrintInfos") *)
About existT.
Print existT.
Print Implicit existT.

Print eq_refl.
About eq_refl.
Print Implicit eq_refl.

Print Nat.add.
About Nat.add.
Print Implicit Nat.add.

About plus_n_O.

Arguments le_S {n} [m] _.
Print le_S.

About comparison.
Print comparison.

Definition foo := forall x, x = 0.
Parameter bar : foo.

Arguments bar {x}.
About bar.
Print bar.

About Peano. (* Module *)
About sym_eq. (* Notation *)

Arguments eq_refl {A} {x}, {A} x.
Print eq_refl.

Definition newdef := fun x:nat => x.

Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
  intros n h h'.
  About n.                              (* search hypothesis *)
  About h.                              (* search hypothesis *)
Abort.

Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False.
  intros n g h h'.
  About g.                              (* search hypothesis *)
  About h.                              (* search hypothesis *)
Abort.

Module Alias := Logic.

About Alias.eq.
About Alias.eq_refl.
About Alias.eq_ind.

Module AboutProj.
Record prod A B := { fst:A ; snd:B }.
About fst.
End AboutProj.

Module AboutPrimProj.
Set Primitive Projections.
Record prod A B := { fst:A ; snd:B }.
About fst.
End AboutPrimProj.

quality99%

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