Raw
and pkind' =
| PTVar of string * pordi list * pkind list |
| PFunc of pkind * pkind |
| PProd of (string * pkind) list * bool |
| PDSum of (string * pkind option) list |
| PKAll of string list * pkind |
| PKExi of string list * pkind |
| POAll of string list * pkind |
| POExi of string list * pkind |
| PFixM of pordi * string * pkind |
| PFixN of pordi * string * pkind |
| PWith of pkind * string * pkind |
| PDPrj of Pos.strloc * string |
| PUCst of pterm * string * pkind |
| PECst of pterm * string * pkind |
| PUVar |
and pterm' =
| PCoer of pterm * pkind |
| PMLet of string list * string list * pkind * string * pterm |
| PLVar of string |
| PLAbs of Pos.strloc * pkind option * pterm * Ast.sugar |
| PAppl of pterm * pterm |
| PReco of (string * pterm) list |
| PProj of pterm * string |
| PCons of string * pterm option |
| PCase of pterm * (string * ppat * pterm) list * (ppat * pterm) option |
| PPrnt of string |
| PFixY of Pos.strloc * int * pterm |
| PAbrt |
and ppat =
| NilPat |
| Simple of (Pos.strloc * pkind option) option |
| Record of (string * (Pos.strloc * pkind option)) list |
val empty_env : env
exception Unbound of string * Pos.popt
val unbound : string Pos.loc -> 'a
exception Arity_error of Pos.popt * string
val arity_error : Pos.popt -> string -> 'a
exception Positivity_error of Pos.popt * string
val positivity_error : Pos.popt -> string -> 'a
val term_variable : env -> Pos.strloc -> Ast.tbox
val ordinal_variable : Ast.occur -> env -> Pos.strloc -> Ast.obox