Re: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML



Am 01.05.2019 um 16:31 schrieb mailing-list anonymous:
> ML ‹
> val f = Const ("HOL.eq", dummyT);
> val A = @{term "A::'b"};
> val q = (f $ A $ A)
>   |> Syntax.check_term @{context}
>   |> Thm.cterm_of @{context};
> ›

Glad you got it to work. Yes, dummyT is treated like a type variable by
type inference, so this is the simplest solution if you just have a
single constant and must figure out the correct type.

Alex




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