Re: [isabelle] "Illegal equation head" ---an error in func definition



On 07/27/2012 09:23 AM, li yongjian wrote:
fun simpBp ::"form \<Rightarrow>  form\<Rightarrow>form\<Rightarrow>tripleSet"
   where
"simpBp (Var n)  h l   =[(Var n,h,l)]"
|"simpBP  (BNot f) h l=simpBP f  l h"
Hi Li,

there is a typo in the second line. You wrote simpBP instead of simpBp. (Isabelle's terms are case-sensitive.)

Lukas






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