Re: [isabelle] Solving a type class constraint

Sounds to me like you just would want to use the type inference itself:

  fun mk_P t = Const (@{const_name P}, dummyT) $ t |>
Syntax.check_term @{context};
  val t = mk_P (Const (@{const_name opt}, dummyT));
  val ct = cterm_of @{theory} t;

This works exactly as expected. Thanks!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.