tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 9 forks source link

Invoking helper function via dot rather than box #268

Open k-mouline opened 3 months ago

k-mouline commented 3 months ago

The following lines:

fun grandpas [p: Person] : set Person { p.(mother+father).father }

pred NoSelfGrandpa { no p: Person | p in p.grandpas }

test expect { nsg : {NoSelfGrandpa} is theorem }

Produce the following error:


  expected: (or/c node? integer?)
  given: #<procedure:...nchmarks/gp-nsg.frg:34:30>
  in: the 1st argument of
      (->
       (or/c node? integer?)
       #:info
       nodeinfo?
       #:op
       symbol?
       node/expr?)
  contract from: 
      (function intexpr->expr/maybe)
  blaming: <pkgs>/forge/lang/ast.rkt
   (assuming the contract is correct)
  at: <pkgs>/forge/lang/ast.rkt:129:18```