Re: [isabelle] primrec

Hi Huub,

On 23/10/2019, 12:54, "cl-isabelle-users-bounces at on behalf of Vromen, H.J. (Huub)" <cl-isabelle-users-bounces at on behalf of H.Vromen at> wrote:

    Could someone tell me what I am doing wrong?

Replace the \equiv with an equality and add more parentheses, like so:

theory Scratch
  imports Main

typedecl w
type_synonym wo = ‹w ⇒ bool›
type_synonym agent = ‹nat›

  reason_to_believe :: ‹agent ⇒ wo ⇒ wo› ("ℛ")

primrec shared_reason_to_believe :: ‹agent ⇒ wo ⇒ wo› ("𝒮ℛ") where
  ‹shared_reason_to_believe 0 p w = (∀i. ℛ i p w)› |
  ‹shared_reason_to_believe (Suc n) p w = (∀i. ℛ i (𝒮ℛ n p) w)›



IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

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