What is the proper way to construct a type application with ML that requires unification? If I just use the
$ constructor I get an expected unification error:
Operator: card_suc :: (?'a × ?'a) set ⇒ (?'a suc × ?'a suc) set Operand: natLeq :: (nat × nat) set
Syntax.check_term ctxt (Const ("Prelim.card_suc", dummyT) $ BNF_Def.bd_of_bnf bnf))
does indeed correctly unify the free variables
Jan van Brügge has marked this topic as resolved.
You picked the last answer from the thread that Lukas linked. However, there was an earlier answer (starting with 'if "term" is something whose type you know ...') that suits your situation better. In fact,
Syntax.check_term does a lot of things and moreover is extensible (so it could do even more things when your code is run in a different context), which makes it something one should avoid using in a definitional package whenever possible.
The problem is the result type, it is not obvious to me how I would construct that from the type of natLeq as input, or better said: Depending on what relation type I get as input
Have a look at the various
mk_... functions in
~~/src/HOL/Tools/BNF/bnf_util.ML for terms and types.
Actually, there is even a
~~/src/HOL/Tools/BNF/bnf_lfp_util.ML, which should be very similar to what you need.
got that to work too:
fun mk_sucT T = Type (\<^type_name>‹suc›, [T]) fun mk_card_suc r = let val T = fst (BNF_Util.dest_relT (fastype_of r)); in Const (\<^const_name>‹card_suc›, BNF_Util.mk_relT (T, T) --> BNF_Util.mk_relT (mk_sucT T, mk_sucT T)) $ r end;
Last updated: Dec 07 2023 at 16:21 UTC