Re: [isabelle] types in higher order logic



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

On 19 Jun 2014, at 14:13, Gergely Buday <gbuday at gmail.com> 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.