Re: [isabelle] primrec



On 23/10/2019 13:53, Vromen, H.J. (Huub) wrote:
> 
> In line 9, I get the error message "Ill-formed equation (expected "lhs = rhs") at
> ⋀p. shared_reason_to_believe 0 p ≡ λw. ∀i. R i p w".
> Could someone tell me what I am doing wrong?

I find it difficult to see anything on this low-resolution screen shot.
Why not make a proper copy-paste of the source text?

You probably merely need to use HOL equality "=" in the proper way. In
applications you rarely see the Pure equality "==" or "≡", although some
users like to confuse other users and (ab)use the latter for its
sometimes more convenient syntax precedence.


	Makarius





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