Re: [isabelle] Solving a type class constraint



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

ML{*
  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!

Lars




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