Re: [isabelle] primrec



Hi Huub,

On 23/10/2019, 12:54, "cl-isabelle-users-bounces at lists.cam.ac.uk on behalf of Vromen, H.J. (Huub)" <cl-isabelle-users-bounces at lists.cam.ac.uk on behalf of H.Vromen at ftr.ru.nl> 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
begin

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

consts
  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)›

end

Thanks,
Dominic


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.