Re: [isabelle] primrec - error: Variable 'a::{} not of sort type



The error message could be more informative, but I can’t imagine why you would use primrec here. There is neither a datatype nor recursion.

Larry Paulson


On 19 Aug 2014, at 12:29, Peter Lammich <lammich at in.tum.de> wrote:

> Hi all.
> 
> If I issue the following definition:
> 
>  primrec f where "f g v (a,b) = (g v a, b)"
> 
> I get:
> 
> Type unification failed: Variable 'a::{} not of sort type
> 
> Type error in application: incompatible operand type
> 
> Operator:  old.rec_prod :: ('b ⇒ 'd ⇒ ??'a) ⇒ 'b × 'd ⇒ ??'a
> Operand:   λa b g v. (g v a, b) ::
>  'b ⇒ 'd ⇒ ('a ⇒ 'b ⇒ 'c) ⇒ 'a ⇒ 'c × 'd
> 
> 
> Although I would have expected the definition to go through. What is
> going wrong here?
> 
> 
> --
>  Peter
> 
> p.s.
> 
>  A quick fix is to either fully declare the type of f, or just write
> primrec f :: "_::type" where ...
> 
> 
> 
> 





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