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 gmail.com> wrote:
> 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