]
type literal =
- [ `Symbol of string
- | `Keyword of string
- | `Number of string
+ [ `Symbol of string * (string option * string option)
+ | `Keyword of string * (string option * string option)
+ | `Number of string * (string option * string option)
]
type case_indtype = string * href option
let apply_prec = 70
let simple_prec = 90
+(* sequents *)
+
+type context_entry =
+ Decl of term
+ | Def of term * term
+
+type sequent = int * context * term
+and context = (string * context_entry) list