Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 19:29:12 -0700 (Fri, 18 Jul 2003)
Revision: 4761
Log message:
Added sequents to <:con< ... >> quotation.
Here's a short summary of syntax:
e ::= sequent [args] { hyps >- con_term list }
args ::= con_term list -- The usual syntax for these terms
hyp ::= <H> | <H[con_terms]>
| <$e$> -- $e$ should be a list of hypothesis terms
| v:con_term
| $v$:con_term
This is the first pass, undoubtly we'll need some tuning.