Am 03.06.2011 10:32, schrieb Guy:
What might --| mean, if not a comment? It doesn't seem possible to define it as an operator.
Obviously, anyone who is going to write a formal logic framework would want to define the following operators ;) :

T |- phi: T proves phi
T |-- phi: T proves phi directly (by application of a single rule)
phi -| T: phi is proven by T
phi --| T: phi is proven by T directly

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to