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



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.