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



The product type is certainly a datatype. I've often used primrec to
define functions over non-recursive datatypes.

- Brian

On Tue, Aug 19, 2014 at 6:27 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 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.