Re: [isabelle] types in higher order logic

Yes, type-checking in Isabelle is static and is essentially Hindley-Milner, augmented with type classes.

On 19 Jun 2014, at 14:13, Gergely Buday <gbuday at> wrote:

> Hi,
> is type inhabitation decidable in Isabelle's higher order logic? I.e. given
> any term t and type T, whether
> G |- t : T
> holds? Is Isabelle/HOL's type system basically Hindley-Milner?
> - Gergely

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