Module Error

Functions collecting error annotations in prooftree

type error =
| Typ of Ast.ordi list * Ast.term * Ast.kind
| Sub of Ast.ordi list * Ast.term * Ast.kind * Ast.kind
| Msg of string
type errors = error list
exception Error of errors
val (&&&) : 'a option -> 'a option -> 'a option
val for_all : ('a -> 'b option) -> 'a list -> 'b option
val check_sub_proof : (Ast.ordi list * Ast.term * Ast.kind * Ast.kind * Ast.sub_rule) -> unit
val check_typ_proof : (Ast.ordi list * Ast.term * Ast.kind * Ast.typ_rule) -> unit
val display_error : Stdlib.Format.formatter -> error -> unit
val display_errors : Stdlib.Format.formatter -> error list -> unit