packages feed

caledon-3.0.0.0: examples/nondet.ncc

#include "../prelude/prelude.ncc"

defn runBoth : bool -> prop
  >| run0 = [A] runBoth A 
                <- putStr "ttt "
                <- A =:= true

  | run1 = [A] runBoth A
                <- putStr "vvvv"
                <- A =:= true

  | run2 = [A] runBoth A
                <- putStr "qqqq"
                <- A =:= true

 >| run3 = [A] runBoth A
                <- putStr " jjj\n"
                <- A =:= false
  
query main = runBoth false