[isabelle] Additional type variable(s) in specification



Hi,

I’m having a problem with function definitions in a locale with type
parameters. I reduced it to the following non-sensical code:

        locale semantic_domain =
          fixes tick :: "'Value ⇒ 'Value"
        begin
        
        function
          myfun :: "unit ⇒ 'Value ⇒ 'Value"
        where
          "myfun () = (λ x. tick (myfun () x))"
        oops

Gives me 
        Additional type variable(s) in specification of "myfun_rel": 'Value 
        Additional type variable(s) in specification of "myfun_dom": 'Value 

It does not happen with the parameter on the LHS:

        function
          myfun :: "unit ⇒ 'Value ⇒ 'Value"
        where
          "myfun () x = tick (myfun () x)"
        
nor with out the locale parameter:

        function
          myfun :: "unit ⇒ 'Value ⇒ 'Value"
        where
          "myfun () = (λ x. (myfun () x))"
        oops

Unfortunately, this does not help me in my real use-case (I’m using
nominal_primrec, not function, and the "λ x" is indeed a "Λ x" from
HOLCF, so I cannot put the argument on the left).

Is there another way to prevent that problem?

Greetings,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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