Skip to Content.
Sympa Menu

maude-help - [[Maude-help] ] random not found

maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[[Maude-help] ] random not found


Chronological Thread 
  • From: Rainer Mann <rainer.mann.rm AT gmx.de>
  • To: maude-help AT lists.cs.illinois.edu
  • Subject: [[Maude-help] ] random not found
  • Date: Tue, 12 Feb 2019 12:10:57 +0100
  • Authentication-results: illinois.edu; spf=pass smtp.mailfrom=rainer.mann.rm AT gmx.de; dmarc=none

In prelude.maude the module RANDOM is defined

fmod RANDOM is
  protecting NAT .
  op random : Nat -> Nat
      [special (id-hook RandomOpSymbol
      op-hook succSymbol (s_ : Nat ~> NzNat))] .
endfm


However, when I try to use the operation random in maude, I get an error

$ maude.darwin64
             \||||||||||||||||||/
           --- Welcome to Maude ---
             /||||||||||||||||||\
       Maude 2.7.1 built: Jun 27 2016 16:43:23
        Copyright 1997-2016 SRI International
           Tue Feb 12 12:09:17 2019
Maude> red random(0) .
Warning: <standard input>, line 1: bad token random.
Warning: <standard input>, line 1: no parse for term.
Maude>


Can anyone tell me what is wrong?

Thanks,
Rainer



Archive powered by MHonArc 2.6.19.

Top of Page