caledon-2.1.0.0: examples/nondet.ncc

defn char : prop  -- builtin
defn putChar    :  char -> prop -- builtin
   | putCharImp = [A] putChar A

defn bool : prop
   | true = bool
   | false = bool

fixity none 1 =:=
defn =:= : {Q} Q -> Q -> prop
   | eq = [a : prop][b:a] (=:=) {Q = a} b b

defn runBoth : bool -> prop
  >| run0 = [A] runBoth A 
                <- putChar 't'
                <- putChar 't'
                <- putChar 't'
                <- putChar 't'
                <- A =:= true

  | run1 = [A] runBoth A
                <- putChar 'v'
                <- putChar 'v'
                <- putChar 'v'
                <- putChar 'v'
                <- A =:= true

  | run2 = [A] runBoth A
                <- putChar 'q'
                <- putChar 'q'
                <- putChar 'q'
                <- putChar 'q'
                <- A =:= true

 >| run3 = [A] runBoth A
                <- putChar 'j'
                <- putChar 'j'
                <- putChar 'j'
                <- putChar 'j'
                <- A =:= false
  
query main = runBoth false