|
(* Check that extra arguments to Arguments do not disturb use of *)
(* scopes in constructors *)
Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
Bind Scope Cminor with stmt.
(* extra argument is ok because of possible coercion to funclass *)
Arguments Scall _ _%Cminor : extra scopes.
(* extra argument is ok because of possible coercion to funclass *)
Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end.
¤ 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.
|
