|
(* Check exportation of Argument Scopes even without import of modules *)
Require Import ZArith.
Module A.
Definition opp := Z.opp.
End A.
Check (A.opp 3).
(* Test extra scopes to be used in the presence of coercions *)
Record B := { f :> Z -> Z }.
Variable a:B.
Arguments a _%Z_scope : extra scopes.
Check a 0.
(* Check that casts activate scopes if ever possible *)
Inductive U := A.
Bind Scope u with U.
Notation "'ε'" := A : u.
Definition c := ε : U.
(* Check activation of type scope for tactics such as assert *)
Goal True.
assert (nat * nat).
Abort.
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
