Jan van Brügge (Sep 15 2021 at 12:36): Jan van Brügge (Sep 15 2021 at 12:36):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
Thanks,
Syntax.check_term ctxt (Const ("Prelim.card_suc", dummyT) $ BNF_Def.bd_of_bnf bnf))
does indeed correctly unify the free variables
Notification Bot (Sep 15 2021 at 13:13):Jan van Brügge has marked this topic as resolved.
Dmitriy Traytel (Sep 15 2021 at 13:20):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.
Jan van Brügge (Sep 15 2021 at 13:23):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
Dmitriy Traytel (Sep 15 2021 at 13:27):Have a look at the various mk_... functions in ~~/src/HOL/Tools/BNF/bnf_util.ML for terms and types.
Dmitriy Traytel (Sep 15 2021 at 13:29):Actually, there is even a mk_cardSuc in ~~/src/HOL/Tools/BNF/bnf_lfp_util.ML, which should be very similar to what you need.
Jan van Brügge (Sep 15 2021 at 13:40):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 21 2024 at 16:20 UTC