# HG changeset patch # User wenzelm # Date 1459343712 -7200 # Node ID 5c672b22dcc2603a41e6f7e7d5e3a4393ab3a685 # Parent aabcc727aa2dc83d9c6391ce3b3f8070920fead5 clarified simple mixfix; diff -r aabcc727aa2d -r 5c672b22dcc2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Mar 30 14:59:12 2016 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Mar 30 15:15:12 2016 +0200 @@ -1960,7 +1960,7 @@ val setT = HOLogic.mk_setT T val elems = HOLogic.mk_set T ts val ([dots], ctxt') = ctxt - |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Delimfix (\...\, Position.no_range))] + |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix.mixfix "...")] (* check expected values *) val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT) val () = diff -r aabcc727aa2d -r 5c672b22dcc2 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Wed Mar 30 14:59:12 2016 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Wed Mar 30 15:15:12 2016 +0200 @@ -42,7 +42,6 @@ (** constants for application and abstraction **) fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); -fun delimfix sy = Delimfix (Input.string sy, Position.no_range); fun add_proof_syntax thy = thy @@ -58,7 +57,7 @@ ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn), ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn), ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn), - ((Binding.make ("MinProof", @{here}), proofT), delimfix "?")] + ((Binding.make ("MinProof", @{here}), proofT), Mixfix.mixfix "?")] |> Sign.add_nonterminals_global [Binding.make ("param", @{here}), Binding.make ("params", @{here})] @@ -67,9 +66,9 @@ ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)), - ("", paramT --> paramT, delimfix "'(_')"), - ("", idtT --> paramsT, delimfix "_"), - ("", paramT --> paramsT, delimfix "_")] + ("", paramT --> paramT, Mixfix.mixfix "'(_')"), + ("", idtT --> paramsT, Mixfix.mixfix "_"), + ("", paramT --> paramsT, Mixfix.mixfix "_")] |> Sign.add_syntax (Print_Mode.ASCII, true) [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)), (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)), diff -r aabcc727aa2d -r 5c672b22dcc2 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Wed Mar 30 14:59:12 2016 +0200 +++ b/src/Pure/Syntax/mixfix.ML Wed Mar 30 15:15:12 2016 +0200 @@ -9,7 +9,6 @@ datatype mixfix = NoSyn | Mixfix of Input.source * int list * int * Position.range | - Delimfix of Input.source * Position.range | Infix of Input.source * int * Position.range | Infixl of Input.source * int * Position.range | Infixr of Input.source * int * Position.range | @@ -20,6 +19,7 @@ signature MIXFIX = sig include BASIC_MIXFIX + val mixfix: string -> mixfix val is_empty: mixfix -> bool val equal: mixfix * mixfix -> bool val range_of: mixfix -> Position.range @@ -42,20 +42,20 @@ datatype mixfix = NoSyn | Mixfix of Input.source * int list * int * Position.range | - Delimfix of Input.source * Position.range | Infix of Input.source * int * Position.range | Infixl of Input.source * int * Position.range | Infixr of Input.source * int * Position.range | Binder of Input.source * int * int * Position.range | Structure of Position.range; +fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range); + fun is_empty NoSyn = true | is_empty _ = false; fun equal (NoSyn, NoSyn) = true | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) = Input.equal_content (sy, sy') andalso ps = ps' andalso p = p' - | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy') | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' @@ -66,7 +66,6 @@ fun range_of NoSyn = Position.no_range | range_of (Mixfix (_, _, _, range)) = range - | range_of (Delimfix (_, range)) = range | range_of (Infix (_, _, range)) = range | range_of (Infixl (_, _, range)) = range | range_of (Infixr (_, _, range)) = range @@ -77,7 +76,6 @@ fun reset_pos NoSyn = NoSyn | reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range) - | reset_pos (Delimfix (sy, _)) = Delimfix (Input.reset_pos sy, Position.no_range) | reset_pos (Infix (sy, p, _)) = Infix (Input.reset_pos sy, p, Position.no_range) | reset_pos (Infixl (sy, p, _)) = Infixl (Input.reset_pos sy, p, Position.no_range) | reset_pos (Infixr (sy, p, _)) = Infixr (Input.reset_pos sy, p, Position.no_range) @@ -100,7 +98,6 @@ fun pretty_mixfix NoSyn = Pretty.str "" | pretty_mixfix (Mixfix (s, ps, p, _)) = parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) - | pretty_mixfix (Delimfix (s, _)) = parens [quoted s] | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) @@ -115,7 +112,6 @@ fun mixfix_args NoSyn = 0 | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy - | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy @@ -141,8 +137,6 @@ fun mfix_of (_, _, NoSyn) = NONE | mfix_of (t, ty, Mixfix (sy, ps, p, range)) = SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range)) - | mfix_of (t, ty, Delimfix (sy, range)) = - SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, Position.set_range range)) | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range) | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range) | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range) @@ -183,8 +177,6 @@ fun mfix_of (_, _, NoSyn) = [] | mfix_of (c, ty, Mixfix (sy, ps, p, range)) = [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)] - | mfix_of (c, ty, Delimfix (sy, range)) = - [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, Position.set_range range)] | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range diff -r aabcc727aa2d -r 5c672b22dcc2 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Mar 30 14:59:12 2016 +0200 +++ b/src/Pure/pure_thy.ML Wed Mar 30 15:15:12 2016 +0200 @@ -23,7 +23,6 @@ val qualify = Binding.qualify true Context.PureN; fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range); -fun delimfix sy = Delimfix (Input.string sy, Position.no_range); fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range); fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range); fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range); @@ -36,7 +35,7 @@ ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))]; val applC_syntax = - [("", typ "'a => cargs", delimfix "_"), + [("", typ "'a => cargs", Mixfix.mixfix "_"), ("_cargs", typ "'a => cargs => cargs", mixfix ("_/ _", [1000, 1000], 1000)), ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)), ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))]; @@ -87,99 +86,99 @@ "class_name"])) #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) #> Sign.add_syntax Syntax.mode_default - [("", typ "prop' => prop", delimfix "_"), - ("", typ "logic => any", delimfix "_"), - ("", typ "prop' => any", delimfix "_"), - ("", typ "logic => logic", delimfix "'(_')"), - ("", typ "prop' => prop'", delimfix "'(_')"), + [("", typ "prop' => prop", Mixfix.mixfix "_"), + ("", typ "logic => any", Mixfix.mixfix "_"), + ("", typ "prop' => any", Mixfix.mixfix "_"), + ("", typ "logic => logic", Mixfix.mixfix "'(_')"), + ("", typ "prop' => prop'", Mixfix.mixfix "'(_')"), ("_constrain", typ "logic => type => logic", mixfix ("_::_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", mixfix ("_::_", [4, 0], 3)), ("_ignore_type", typ "'a", NoSyn), - ("", typ "tid_position => type", delimfix "_"), - ("", typ "tvar_position => type", delimfix "_"), - ("", typ "type_name => type", delimfix "_"), - ("_type_name", typ "id => type_name", delimfix "_"), - ("_type_name", typ "longid => type_name", delimfix "_"), + ("", typ "tid_position => type", Mixfix.mixfix "_"), + ("", typ "tvar_position => type", Mixfix.mixfix "_"), + ("", typ "type_name => type", Mixfix.mixfix "_"), + ("_type_name", typ "id => type_name", Mixfix.mixfix "_"), + ("_type_name", typ "longid => type_name", Mixfix.mixfix "_"), ("_ofsort", typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)), ("_ofsort", typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)), ("_dummy_ofsort", typ "sort => type", mixfix ("'_()::_", [0], 1000)), - ("", typ "class_name => sort", delimfix "_"), - ("_class_name", typ "id => class_name", delimfix "_"), - ("_class_name", typ "longid => class_name", delimfix "_"), - ("_topsort", typ "sort", delimfix "{}"), - ("_sort", typ "classes => sort", delimfix "{_}"), - ("", typ "class_name => classes", delimfix "_"), - ("_classes", typ "class_name => classes => classes", delimfix "_,_"), + ("", typ "class_name => sort", Mixfix.mixfix "_"), + ("_class_name", typ "id => class_name", Mixfix.mixfix "_"), + ("_class_name", typ "longid => class_name", Mixfix.mixfix "_"), + ("_topsort", typ "sort", Mixfix.mixfix "{}"), + ("_sort", typ "classes => sort", Mixfix.mixfix "{_}"), + ("", typ "class_name => classes", Mixfix.mixfix "_"), + ("_classes", typ "class_name => classes => classes", Mixfix.mixfix "_,_"), ("_tapp", typ "type => type_name => type", mixfix ("_ _", [1000, 0], 1000)), - ("_tappl", typ "type => types => type_name => type", delimfix "((1'(_,/ _')) _)"), - ("", typ "type => types", delimfix "_"), - ("_types", typ "type => types => types", delimfix "_,/ _"), + ("_tappl", typ "type => types => type_name => type", Mixfix.mixfix "((1'(_,/ _')) _)"), + ("", typ "type => types", Mixfix.mixfix "_"), + ("_types", typ "type => types => types", Mixfix.mixfix "_,/ _"), ("\<^type>fun", typ "type => type => type", mixfix ("(_/ \ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", mixfix ("([_]/ \ _)", [0, 0], 0)), - ("", typ "type => type", delimfix "'(_')"), - ("\<^type>dummy", typ "type", delimfix "'_"), + ("", typ "type => type", Mixfix.mixfix "'(_')"), + ("\<^type>dummy", typ "type", Mixfix.mixfix "'_"), ("_type_prop", typ "'a", NoSyn), ("_lambda", typ "pttrns => 'a => logic", mixfix ("(3\_./ _)", [0, 3], 3)), ("_abs", typ "'a", NoSyn), - ("", typ "'a => args", delimfix "_"), - ("_args", typ "'a => args => args", delimfix "_,/ _"), - ("", typ "id_position => idt", delimfix "_"), - ("_idtdummy", typ "idt", delimfix "'_"), + ("", typ "'a => args", Mixfix.mixfix "_"), + ("_args", typ "'a => args => args", Mixfix.mixfix "_,/ _"), + ("", typ "id_position => idt", Mixfix.mixfix "_"), + ("_idtdummy", typ "idt", Mixfix.mixfix "'_"), ("_idtyp", typ "id_position => type => idt", mixfix ("_::_", [], 0)), ("_idtypdummy", typ "type => idt", mixfix ("'_()::_", [], 0)), - ("", typ "idt => idt", delimfix "'(_')"), - ("", typ "idt => idts", delimfix "_"), + ("", typ "idt => idt", Mixfix.mixfix "'(_')"), + ("", typ "idt => idts", Mixfix.mixfix "_"), ("_idts", typ "idt => idts => idts", mixfix ("_/ _", [1, 0], 0)), - ("", typ "idt => pttrn", delimfix "_"), - ("", typ "pttrn => pttrns", delimfix "_"), + ("", typ "idt => pttrn", Mixfix.mixfix "_"), + ("", typ "pttrn => pttrns", Mixfix.mixfix "_"), ("_pttrns", typ "pttrn => pttrns => pttrns", mixfix ("_/ _", [1, 0], 0)), - ("", typ "aprop => aprop", delimfix "'(_')"), - ("", typ "id_position => aprop", delimfix "_"), - ("", typ "longid_position => aprop", delimfix "_"), - ("", typ "var_position => aprop", delimfix "_"), - ("_DDDOT", typ "aprop", delimfix "\"), - ("_aprop", typ "aprop => prop", delimfix "PROP _"), - ("_asm", typ "prop => asms", delimfix "_"), - ("_asms", typ "prop => asms => asms", delimfix "_;/ _"), + ("", typ "aprop => aprop", Mixfix.mixfix "'(_')"), + ("", typ "id_position => aprop", Mixfix.mixfix "_"), + ("", typ "longid_position => aprop", Mixfix.mixfix "_"), + ("", typ "var_position => aprop", Mixfix.mixfix "_"), + ("_DDDOT", typ "aprop", Mixfix.mixfix "\"), + ("_aprop", typ "aprop => prop", Mixfix.mixfix "PROP _"), + ("_asm", typ "prop => asms", Mixfix.mixfix "_"), + ("_asms", typ "prop => asms => asms", Mixfix.mixfix "_;/ _"), ("_bigimpl", typ "asms => prop => prop", mixfix ("((1\_\)/ \ _)", [0, 1], 1)), - ("_ofclass", typ "type => logic => prop", delimfix "(1OFCLASS/(1'(_,/ _')))"), + ("_ofclass", typ "type => logic => prop", Mixfix.mixfix "(1OFCLASS/(1'(_,/ _')))"), ("_mk_ofclass", typ "dummy", NoSyn), - ("_TYPE", typ "type => logic", delimfix "(1TYPE/(1'(_')))"), - ("", typ "id_position => logic", delimfix "_"), - ("", typ "longid_position => logic", delimfix "_"), - ("", typ "var_position => logic", delimfix "_"), - ("_DDDOT", typ "logic", delimfix "\"), + ("_TYPE", typ "type => logic", Mixfix.mixfix "(1TYPE/(1'(_')))"), + ("", typ "id_position => logic", Mixfix.mixfix "_"), + ("", typ "longid_position => logic", Mixfix.mixfix "_"), + ("", typ "var_position => logic", Mixfix.mixfix "_"), + ("_DDDOT", typ "logic", Mixfix.mixfix "\"), ("_strip_positions", typ "'a", NoSyn), - ("_position", typ "num_token => num_position", delimfix "_"), - ("_position", typ "float_token => float_position", delimfix "_"), - ("_constify", typ "num_position => num_const", delimfix "_"), - ("_constify", typ "float_position => float_const", delimfix "_"), - ("_index", typ "logic => index", delimfix "(00\<^bsub>_\<^esub>)"), - ("_indexdefault", typ "index", delimfix ""), - ("_indexvar", typ "index", delimfix "'\"), + ("_position", typ "num_token => num_position", Mixfix.mixfix "_"), + ("_position", typ "float_token => float_position", Mixfix.mixfix "_"), + ("_constify", typ "num_position => num_const", Mixfix.mixfix "_"), + ("_constify", typ "float_position => float_const", Mixfix.mixfix "_"), + ("_index", typ "logic => index", Mixfix.mixfix "(00\<^bsub>_\<^esub>)"), + ("_indexdefault", typ "index", Mixfix.mixfix ""), + ("_indexvar", typ "index", Mixfix.mixfix "'\"), ("_struct", typ "index => logic", NoSyn), ("_update_name", typ "idt", NoSyn), ("_constrainAbs", typ "'a", NoSyn), - ("_position_sort", typ "tid => tid_position", delimfix "_"), - ("_position_sort", typ "tvar => tvar_position", delimfix "_"), - ("_position", typ "id => id_position", delimfix "_"), - ("_position", typ "longid => longid_position", delimfix "_"), - ("_position", typ "var => var_position", delimfix "_"), - ("_position", typ "str_token => str_position", delimfix "_"), - ("_position", typ "string_token => string_position", delimfix "_"), - ("_position", typ "cartouche => cartouche_position", delimfix "_"), + ("_position_sort", typ "tid => tid_position", Mixfix.mixfix "_"), + ("_position_sort", typ "tvar => tvar_position", Mixfix.mixfix "_"), + ("_position", typ "id => id_position", Mixfix.mixfix "_"), + ("_position", typ "longid => longid_position", Mixfix.mixfix "_"), + ("_position", typ "var => var_position", Mixfix.mixfix "_"), + ("_position", typ "str_token => str_position", Mixfix.mixfix "_"), + ("_position", typ "string_token => string_position", Mixfix.mixfix "_"), + ("_position", typ "cartouche => cartouche_position", Mixfix.mixfix "_"), ("_type_constraint_", typ "'a", NoSyn), - ("_context_const", typ "id_position => logic", delimfix "CONST _"), - ("_context_const", typ "id_position => aprop", delimfix "CONST _"), - ("_context_const", typ "longid_position => logic", delimfix "CONST _"), - ("_context_const", typ "longid_position => aprop", delimfix "CONST _"), - ("_context_xconst", typ "id_position => logic", delimfix "XCONST _"), - ("_context_xconst", typ "id_position => aprop", delimfix "XCONST _"), - ("_context_xconst", typ "longid_position => logic", delimfix "XCONST _"), - ("_context_xconst", typ "longid_position => aprop", delimfix "XCONST _"), - (const "Pure.dummy_pattern", typ "aprop", delimfix "'_"), - ("_sort_constraint", typ "type => prop", delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), - (const "Pure.term", typ "logic => prop", delimfix "TERM _"), + ("_context_const", typ "id_position => logic", Mixfix.mixfix "CONST _"), + ("_context_const", typ "id_position => aprop", Mixfix.mixfix "CONST _"), + ("_context_const", typ "longid_position => logic", Mixfix.mixfix "CONST _"), + ("_context_const", typ "longid_position => aprop", Mixfix.mixfix "CONST _"), + ("_context_xconst", typ "id_position => logic", Mixfix.mixfix "XCONST _"), + ("_context_xconst", typ "id_position => aprop", Mixfix.mixfix "XCONST _"), + ("_context_xconst", typ "longid_position => logic", Mixfix.mixfix "XCONST _"), + ("_context_xconst", typ "longid_position => aprop", Mixfix.mixfix "XCONST _"), + (const "Pure.dummy_pattern", typ "aprop", Mixfix.mixfix "'_"), + ("_sort_constraint", typ "type => prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), + (const "Pure.term", typ "logic => prop", Mixfix.mixfix "TERM _"), (const "Pure.conjunction", typ "prop => prop => prop", infixr_ ("&&&", 2))] #> Sign.add_syntax Syntax.mode_default applC_syntax #> Sign.add_syntax (Print_Mode.ASCII, true) @@ -189,9 +188,9 @@ (const "Pure.eq", typ "'a => 'a => prop", infix_ ("==", 2)), (const "Pure.all_binder", typ "idts => prop => prop", mixfix ("(3!!_./ _)", [0, 0], 0)), (const "Pure.imp", typ "prop => prop => prop", infixr_ ("==>", 1)), - ("_DDDOT", typ "aprop", delimfix "..."), + ("_DDDOT", typ "aprop", Mixfix.mixfix "..."), ("_bigimpl", typ "asms => prop => prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), - ("_DDDOT", typ "logic", delimfix "...")] + ("_DDDOT", typ "logic", Mixfix.mixfix "...")] #> Sign.add_syntax ("", false) [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))] #> Sign.add_consts @@ -200,7 +199,7 @@ (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\", 0, 0)), (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), - (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", delimfix "'_")] + (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Mixfix.mixfix "'_")] #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) [] #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) [] #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []