Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more operations;
authorwenzelm
Sun, 20 Oct 2024 18:47:42 +0200
changeset 81212 b5836dd39018
parent 81211 f6d73a2b3b39
child 81213 d1170873976e
more operations;
src/Pure/Syntax/mixfix.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/mixfix.ML	Sun Oct 20 15:48:06 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sun Oct 20 18:47:42 2024 +0200
@@ -30,6 +30,7 @@
   val default_constraint: Proof.context -> mixfix -> typ
   val make_type: int -> typ
   val binder_name: string -> string
+  val is_binder_name: string -> bool
   val syn_ext_types: Proof.context -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
   val syn_ext_consts: Proof.context -> string list -> (string * typ * mixfix) list ->
     Syntax_Ext.syn_ext
@@ -170,7 +171,9 @@
 (* binder notation *)
 
 val binder_stamp = stamp ();
-val binder_name = suffix "_binder";
+val binder_suffix = "_binder"
+val binder_name = suffix binder_suffix;
+val is_binder_name = String.isSuffix binder_suffix;
 
 val binder_bg = Symbol_Pos.explode0 "(";
 val binder_en = Symbol_Pos.explode0 "_./ _)";
isabelle