Quelle PrintMatch.v Sprache: Coq

(* NB feel free to add other tests about printing match, not just about Match All Subterms *)

Module MatchAllSubterms.

Set Printing Match All Subterms.
Set Printing Universes.

Polymorphic Inductive eqT@{u} {A:Type@{u}} (a:A) : A -> Type@{u} := reflT : eqT a a.
Print eqT_rect.

Set Definitional UIP.
Inductive seq {A} (a:A) : A -> SProp := srefl : seq a a.
Print seq_rect.

End MatchAllSubterms.

Module Bug18163.

Set Printing All.
Print eq_sym.
Unset Printing All.

Set Printing Implicit.
Print eq_sym.

Set Asymmetric Patterns.
Print eq_sym.

End Bug18163.

Module AvoidName.

Definition test (O : unit) (S : nat -> unit) (n : nat) :=
match n with
| Datatypes.O => O
| Datatypes.S n => S n
end.

Print test.

End AvoidName.

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.