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

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 `mk_cardSuc`

in `~~/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: Feb 27 2024 at 08:17 UTC