Commit 9fa6da6d authored by Andrei Paskevich's avatar Andrei Paskevich

do not put spaces around colon in metas and labels

parent fe983f1d
......@@ -8,7 +8,7 @@ end
theory Partial_incomplete
meta "enco_kept" "instantiate"
meta "encoding_instantiate : complete" "no"
meta "encoding_instantiate:complete" "no"
end
theory Poly_explicit
......@@ -74,6 +74,6 @@ end
theory KeptIntReal
use int.Int
use real.Real
meta "encoding : kept" type Int.int
meta "encoding : kept" type Real.real
meta "encoding:kept" type Int.int
meta "encoding:kept" type Real.real
end
......@@ -28,7 +28,7 @@ theory BuiltIn
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
meta "encoding:kept" type int
end
theory int.Int
......
......@@ -45,8 +45,8 @@ theory BuiltIn
syntax type int "$int"
syntax type real "$real"
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "encoding:kept" type int
meta "encoding:kept" type real
meta "eliminate_algebraic" "no_index"
end
......@@ -146,7 +146,7 @@ end
theory tptp.Univ
syntax type iType "$i"
meta "encoding : kept" type iType
meta "encoding:kept" type iType
end
theory tptp.IntTrunc
......@@ -214,7 +214,7 @@ theory tptp.Rat
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type rat
meta "encoding:kept" type rat
end
theory tptp.RatTrunc
......
......@@ -34,7 +34,7 @@ theory BuiltIn
syntax type real "REAL"
syntax predicate (=) "(%1 = %2)"
meta "encoding : kept" type int
meta "encoding:kept" type int
end
theory int.Int
......@@ -117,7 +117,7 @@ theory real.Real
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
meta "encoding:kept" type real
end
......@@ -138,7 +138,7 @@ theory Bool
syntax type bool "BITVECTOR(1)"
syntax function True "0bin1"
syntax function False "0bin0"
meta "encoding : kept" type bool
meta "encoding:kept" type bool
end
theory bool.Bool
......@@ -153,12 +153,12 @@ theory HighOrd
meta "material_type_arg" type (->), 1
syntax function (@) "(%1[%2])"
meta "encoding : lskept" function (@)
meta "encoding:lskept" function (@)
end
theory map.Map
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:lskept" function get
meta "encoding:lskept" function set
syntax function get "(%1[%2])"
syntax function set "(%1 WITH [%2] := %3)"
......
......@@ -55,9 +55,9 @@ theory int.Int
meta "gappa arith" predicate (<), "not ", ">=", "<="
meta "gappa arith" predicate (>), "not ", "<=", ">="
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
remove prop NonTrivialRing
remove prop ZeroLessOne
......@@ -101,9 +101,9 @@ theory real.Real
meta "gappa arith" predicate (<), "not ", ">=", "<="
meta "gappa arith" predicate (>), "not ", "<=", ">="
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
remove prop NonTrivialRing
remove prop ZeroLessOne
......@@ -152,14 +152,14 @@ end
theory floating_point.Single
syntax function round "float<ieee_32,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
meta "instantiate:auto" prop Bounded_value
end
theory floating_point.Double
syntax function round "float<ieee_64,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
meta "instantiate:auto" prop Bounded_value
end
......@@ -167,7 +167,7 @@ end
theory floating_point.SingleMultiRounding
syntax function round "float<ieee_32,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
meta "instantiate:auto" prop Bounded_value
end
*)
......@@ -175,7 +175,7 @@ end
theory floating_point.DoubleMultiRounding
syntax function round "float<ieee_64,%1>(%2)"
meta "instantiate : auto" prop Bounded_value
meta "instantiate:auto" prop Bounded_value
end
......
......@@ -36,7 +36,7 @@ theory BuiltIn
syntax type real "Reals"
syntax predicate (=) "(%1 == %2)"
meta "encoding : kept" type int
meta "encoding:kept" type int
end
(* int *)
......@@ -58,9 +58,9 @@ theory int.Int
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
......@@ -82,7 +82,7 @@ theory int.Int
remove prop CompatOrderMult
remove prop ZeroLessOne
meta "encoding : kept" type int
meta "encoding:kept" type int
end
theory int.Abs
......@@ -102,7 +102,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
meta "encoding : kept" type int
meta "encoding:kept" type int
end
(* real *)
......@@ -126,9 +126,9 @@ theory real.Real
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
remove prop MulComm.Comm
remove prop MulAssoc.Assoc
......@@ -158,7 +158,7 @@ theory real.Real
remove prop assoc_div_div
remove prop CompatOrderMult
(*meta "encoding : kept" type real*)
(*meta "encoding:kept" type real*)
end
theory real.Abs
......@@ -248,7 +248,7 @@ theory Bool
syntax type bool "Bool"
syntax function True "True"
syntax function False "False"
meta "encoding : kept" type bool
meta "encoding:kept" type bool
end
theory bool.Bool
......
......@@ -32,7 +32,7 @@ theory BuiltIn
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
meta "encoding:kept" type int
end
theory int.Int
......@@ -113,7 +113,7 @@ theory real.Real
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
meta "encoding:kept" type real
end
......@@ -121,7 +121,7 @@ theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
meta "encoding:kept" type bool
end
theory bool.Bool
......@@ -134,7 +134,7 @@ end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:lskept" function ite
end
(* needs to be checked
......@@ -171,18 +171,18 @@ theory HighOrd
meta "material_type_arg" type (->), 1
syntax function (@) "(select %1 %2)"
meta "encoding : lskept" function (@)
meta "encoding:lskept" function (@)
end
theory map.Map
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:lskept" function get
meta "encoding:lskept" function set
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
end
theory map.Const
meta "encoding : lskept" function const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
......@@ -46,9 +46,9 @@ transformation "encoding_tptp"
theory BuiltIn
(* support for integers disabled because may be inconsistent
meta "encoding : kept" type int
meta "encoding:kept" type int
*)
meta "encoding : base" type real
meta "encoding:base" type real
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
......@@ -72,9 +72,9 @@ theory real.Real
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
(* These follow from Metitarski's axioms. *)
remove prop MulComm.Comm
......
......@@ -33,7 +33,7 @@ transformation "discriminate"
transformation "encoding_tptp"
theory BuiltIn
meta "encoding : base" type real
meta "encoding:base" type real
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
......@@ -57,9 +57,9 @@ theory real.Real
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
meta "inline : no" predicate (<=)
meta "inline : no" predicate (>=)
meta "inline : no" predicate (>)
meta "inline:no" predicate (<=)
meta "inline:no" predicate (>=)
meta "inline:no" predicate (>)
remove allprops
end
......
......@@ -45,8 +45,8 @@ theory BuiltIn
syntax type int "$int"
syntax type real "$real"
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "encoding:kept" type int
meta "encoding:kept" type real
meta "eliminate_algebraic" "no_index"
end
......@@ -143,7 +143,7 @@ end
theory tptp.Univ
syntax type iType "$i"
meta "encoding : kept" type iType
meta "encoding:kept" type iType
end
theory tptp.IntTrunc
......@@ -211,7 +211,7 @@ theory tptp.Rat
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type rat
meta "encoding:kept" type rat
end
theory tptp.RatTrunc
......
......@@ -70,7 +70,7 @@ theory real.Real
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
meta "encoding:kept" type real
end
......@@ -79,7 +79,7 @@ theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
meta "encoding:kept" type bool
end
theory bool.Bool
......@@ -92,7 +92,7 @@ end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:lskept" function ite
end
*)
......
......@@ -34,7 +34,7 @@ transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(EQ %1 %2)"
meta "encoding : base" type int
meta "encoding:base" type int
end
theory int.Int
......
......@@ -28,7 +28,7 @@ theory BuiltIn
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
meta "encoding:kept" type int
end
theory int.Int
......@@ -108,7 +108,7 @@ theory real.Real
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
meta "encoding:kept" type real
end
......@@ -116,7 +116,7 @@ theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
meta "encoding:kept" type bool
end
theory bool.Bool
......@@ -129,7 +129,7 @@ end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
meta "encoding:lskept" function ite
meta "encoding:ignore_polymorphism_ls" function ite
end
......@@ -146,7 +146,7 @@ theory HighOrd
meta "material_type_arg" type (->), 1
syntax function (@) "(select %1 %2)"
meta "encoding : lskept" function (@)
meta "encoding:lskept" function (@)
meta "encoding:ignore_polymorphism_ts" type (->)
end
......@@ -154,8 +154,8 @@ end
theory map.Map
syntax function get "(select %1 %2)"
syntax function set "(store %1 %2 %3)"
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:lskept" function get
meta "encoding:lskept" function set
meta "encoding:ignore_polymorphism_ls" function get
meta "encoding:ignore_polymorphism_ls" function ([])
meta "encoding:ignore_polymorphism_ls" function set
......@@ -168,6 +168,6 @@ theory map.Map
end
theory map.Const
meta "encoding : lskept" function const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
......@@ -40,8 +40,8 @@ theory BuiltIn
syntax type int "$int"
syntax type real "$real"
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "encoding:kept" type int
meta "encoding:kept" type real
meta "eliminate_algebraic" "no_index"
end
......@@ -138,7 +138,7 @@ end
theory tptp.Univ
syntax type iType "$i"
meta "encoding : kept" type iType
meta "encoding:kept" type iType
end
theory tptp.IntTrunc
......@@ -206,7 +206,7 @@ theory tptp.Rat
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type rat
meta "encoding:kept" type rat
end
theory tptp.RatTrunc
......
......@@ -29,13 +29,13 @@ theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "encoding:ignore_polymorphism_ls" predicate (=)
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "encoding:kept" type int
meta "encoding:kept" type real
end
theory map.Map
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:lskept" function get
meta "encoding:lskept" function set
meta "encoding:ignore_polymorphism_ts" type map
meta "encoding:ignore_polymorphism_ls" function get
......
......@@ -33,7 +33,7 @@ theory BuiltIn
syntax type real "real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
meta "encoding:kept" type int
(* could we do this? *)
(* meta "eliminate_algebraic" "keep_enums" *)
......@@ -119,14 +119,14 @@ theory real.Real
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
meta "encoding:kept" type real
end
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
meta "encoding:kept" type bool
end
theory bool.Bool
......@@ -140,12 +140,12 @@ theory HighOrd
meta "material_type_arg" type (->), 1
syntax function (@) "(%1 %2)"
meta "encoding : lskept" function (@)
meta "encoding:lskept" function (@)
end
theory map.Map
meta "encoding : lskept" function get
meta "encoding : lskept" function set
meta "encoding:lskept" function get
meta "encoding:lskept" function set
syntax function get "(%1 %2)"
syntax function ([]) "(%1 %2)"
......@@ -154,5 +154,5 @@ theory map.Map
end
theory map.Const
meta "encoding : lskept" function const
meta "encoding:lskept" function const
end
......@@ -29,7 +29,7 @@ theory BuiltIn
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "encoding : kept" type int
meta "encoding:kept" type int
end
theory int.Int
......@@ -110,7 +110,7 @@ theory real.Real
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
meta "encoding:kept" type real
end
......@@ -120,7 +120,7 @@ theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
meta "encoding_decorate : kept" type bool
meta "encoding_decorate:kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
......
......@@ -81,9 +81,9 @@ module M
function projf_r_g "model_trace:.g" (x : r) : bool
=
x.g
meta "inline : no" function projf_r_f
meta "inline:no" function projf_r_f
meta "model_projection" function projf_r_f
meta "inline : no" function projf_r_g
meta "inline:no" function projf_r_g
meta "model_projection" function projf_r_g
let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
......@@ -133,10 +133,10 @@ module M
=
rec_map.g_bool
meta "inline : no" function projf_r_map_f_map
meta "inline:no" function projf_r_map_f_map
meta "model_projection" function projf_r_map_f_map
meta "inline : no" function projf_r_map_g
meta "inline:no" function projf_r_map_g
meta "model_projection" function projf_r_map_g
(* Tests *)
......@@ -164,7 +164,7 @@ module M
function projfi "model_trace:.projfi" (l : int) : int
= l
meta "inline : no" function projfi
meta "inline:no" function projfi
meta "model_projection" function projfi
function projf1 "model_trace:.projf1" (l : int) : bool
......@@ -175,9 +175,9 @@ module M
=
l <= 0
meta "inline : no" function projf1
meta "inline:no" function projf1
meta "model_projection" function projf1
meta "inline : no" function projf2
meta "inline:no" function projf2
meta "model_projection" function projf2
(*******************************************************
......@@ -211,7 +211,7 @@ module M
| Cons (Integer n) _ -> n
| _ -> 0
end
meta "inline : no" function projfl
meta "inline:no" function projfl
meta "model_projection" function projfl
(* list int_type will be projected using projfl to int,
......
......@@ -279,7 +279,6 @@ let create_debugging_trans trans_name (tran : Task.task trans) =
print_task_goal t2;
Debug.dprintf debug "@.@.";
t2;
end in
store new_trans
......@@ -368,18 +367,18 @@ let on_flag_find m ft s = try Hstr.find ft s with
let on_flag_gen m ft def_name def arg =
on_meta_excl m (fun alo ->
let t, tr_name = match alo with
| None -> def, Printf.sprintf "%s %s" m.meta_name def_name
| None -> def, Printf.sprintf "%s%s" m.meta_name def_name
| Some [MAstr s] ->
on_flag_find m ft s, Printf.sprintf "%s : %s" m.meta_name s
on_flag_find m ft s, Printf.sprintf "%s:%s" m.meta_name s
| _ -> raise (IllegalFlagTrans m)
in
named tr_name (t arg))
let on_flag m ft def arg =
let tdef x = on_flag_find m ft def x in
on_flag_gen m ft (Printf.sprintf ": %s" def) tdef arg
let on_flag m ft def_name arg =
let def x = on_flag_find m ft def_name x in
on_flag_gen m ft (Printf.sprintf ":%s" def_name) def arg
let on_flag_t m ft def arg = on_flag_gen m ft "(default)" def arg
let on_flag_t m ft def arg = on_flag_gen m ft " (default)" def arg
let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownTrans s ->
......
......@@ -17,22 +17,22 @@ open Decl
open Theory
open Task
let meta_inst = register_meta "encoding : inst" [MTty]
let meta_inst = register_meta "encoding:inst" [MTty]
~desc:"Specify@ which@ types@ should@ instantiate@ symbols@ marked@ by@ \
'encoding : lskept'."
'encoding:lskept'."
let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
let meta_lskept = register_meta "encoding:lskept" [MTlsymbol]
~desc:"Specify@ which@ function/predicate@ symbols@ should@ be@ kept.@ \
When@ the@ symbol@ is@ polymorphic,@ generate@ every@ possible@ \
type@ instances@ with@ types@ marked@ by@ 'encoding : inst'."
type@ instances@ with@ types@ marked@ by@ 'encoding:inst'."
let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
let meta_lsinst = register_meta "encoding:lsinst" [MTlsymbol;MTlsymbol]
~desc:"Specify@ which@ type@ instances@ of@ symbols@ should@ be@ kept.@ \
The first@ symbol@ specifies@ the@ polymorphic@ symbol,@ \
the@ second@ provides@ a@ monomorphic@ type@ signature@ to@ keep."
let meta_select_inst = register_meta_excl "select_inst" [MTstring]
~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : inst':@; \
~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding:inst':@; \
@[\
- none: @[don't@ mark@ any@ type@ automatically@]@\n\
- goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\
......@@ -40,7 +40,7 @@ let meta_select_inst = register_meta_excl "select_inst" [MTstring]
@]"
let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lskept':@; \
~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding:lskept':@; \
@[\
- none: @[don't@ mark@ any@ symbol@ automatically@]@\n\
- goal: @[mark@ every@ polymorphic@ symbol@ in@ the@ goal@]@\n\
......@@ -48,7 +48,7 @@ let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
@]"
let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lsinst':@; \
~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding:lsinst':@; \
@[\
- none: @[don't@ mark@ any@ symbol@ automatically@]@\n\
- goal: @[mark@ every@ monomorphic@ instance@ in@ the@ goal@]@\n\
......
......@@ -430,10 +430,10 @@ let eliminate_match =
let meta_elim = register_meta "eliminate_algebraic" [MTstring]
~desc:"@[<hov 2>Configure the 'eliminate_algebraic' transformation:@\n\
\"keep_types\" : @[keep algebraic type definitions@]@\n\
\"keep_enums\" : @[keep monomorphic enumeration types@]@\n\
\"keep_recs\" : @[keep non-recursive records@]@\n\
\"no_index\" : @[do not generate indexing functions@]@]"
- keep_types: @[keep algebraic type definitions@]@\n\
- keep_enums: @[keep monomorphic enumeration types@]@\n\
- keep_recs: @[keep non-recursive records@]@\n\
- no_index: @[do not generate indexing functions@]@]"
let eliminate_algebraic = Trans.compose compile_match
(Trans.on_meta meta_elim (fun ml ->
......
......@@ -16,7 +16,7 @@ open Task
open Trans
let meta_select_kept = register_meta_excl "select_kept" [MTstring]
~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : kept':@; \
~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding:kept':@; \
@[\
- none: @[don't@ mark@ any@ type@ automatically@]@\n\
- goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\
......@@ -40,7 +40,7 @@ let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
- @[<hov 2>tags: protect@ variables@ in@ equalities@ \
with@ type@ annotations@]@\n\
- @[<hov 2>guards: protect@ variables@ in@ equalities@ \
with@ type@ conditions@]\n\
with@ type@ conditions@]@\n\
- @[<hov 2>tags_full: put@ type@ annotations@ on@ top@ \
of@ every@ term@]@\n\
- @[<hov 2>guards_full: add@ type@ conditions@ for@ every@ variable.@]\
......
......@@ -79,7 +79,7 @@ let fold in_goal notdeft notdeff notls task_hd (env, task) =
(* transformations *)
let meta = Theory.register_meta "inline : no" [Theory.MTlsymbol]
let meta = Theory.register_meta "inline:no" [Theory.MTlsymbol]
~desc:"Disallow@ the@ inlining@ of@ the@ given@ function/predicate@ symbol."
let t ?(use_meta=true) ?(in_goal=false) ~notdeft ~notdeff ~notls =
......
......@@ -31,7 +31,7 @@ val t :
- [ls] is a function symbol and [notdeft] returns true on its definition;
- [ls] is a predicate symbol and [notdeff] returns true on its definition;
- [notls ls] returns [true];
- [use_meta] is set and [ls] is tagged by "inline : no"
- [use_meta] is set and [ls] is tagged by "inline:no"
Notice that [use_meta], [notdeft], [notdeff], [notls] restrict only which
symbols are inlined not when.
......