DeclareScope t_scope. DelimitScope t_scope with ts.
Import PrimString. Inductive t := v : string -> t. Definition parse : string -> t := v. Definitionprint : t -> string := fun x => match x with v s => s end.
String Notation t parse print : t_scope. Check v "bla". (* string notation not used: [v "bla"] *)
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.
