[isabelle] primrec

I am trying to formalize David Lewis' account of common knowledge. My theory starts with:


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?

Huub Vromen
Radboud University-Nijmegen, Department of Philosophy
Room E 16.11
Erasmusplein 1, 6525 HT  Nijmegen, Netherlands

Attachment: Attachment.tiff
Description: Attachment.tiff

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