Term
Terms of our language.
An expression.
and desc =
| Coh of string * (icit * string * t) list * t * substitution
coherence
*)| Var of string
variable
*)| Abs of icit * string * t * t
abstraction
*)| App of icit * t * t
application
*)| Pi of icit * string * t * t
Π-type
*)| Id of t * t * t
identity type
*)| Arr of t * t * t
arrow type
*)| Hom of t * t
internal hom type
*)| Prod of t * t
product type
*)| Op of t
opposite of a type
*)| One
terminal type
*)| Meta of meta
a variable to be unified
*)| Obj
object type
*)| Type
the type of types
*)and context = (string * t) list
and substitution = (string * t) list
and meta = {
id : int;
source_pos : Extlib.Pos.t option;
position in the source code (can be empty if the metavariable was created on the fly)
*)mutable value : t option;
ty : t;
}
val is_pi : t -> bool
val to_string : ?pa:bool -> t -> string
String representation of an expression. This should mostly be useful for debugging (we want to print values).
val string_of_context : (string * t) list -> string
val mk : ?pos:Extlib.Pos.t -> desc -> t
Create an expression from its contents.
val repos : Extlib.Pos.t -> t -> t
Change the position.
val var : ?pos:Extlib.Pos.t -> string -> t
val meta : ?pos:Extlib.Pos.t -> ?real:bool -> ?value:t -> t -> t
val hole : ?pos:Extlib.Pos.t -> ?real:bool -> unit -> t
val abs_coh : ?pos:Extlib.Pos.t -> string -> (icit * string * t) list -> t -> t
Create coherence with abstracted arguments.
type prog = command list
A program.
val fresh_var : string -> t
val homs : ?pos:Extlib.Pos.t -> t list -> t -> t
Build multiple hom types.
val abss : ?pos:Extlib.Pos.t -> (icit * string * t) list -> t -> t
Build multiple abstractions.
val pis : ?pos:Extlib.Pos.t -> (icit * string * t) list -> t -> t
Build multiple pi types.
val pis_explicit : ?pos:Extlib.Pos.t -> (string * t) list -> t -> t
Build multiple pi types.
val prods : ?pos:Extlib.Pos.t -> t list -> t
Build multiple products.
val has_fv : string -> t -> bool
val is_var : t -> bool
val is_obj : t -> bool
val is_implicit_pi : t -> bool
val is_metavariable : t -> bool
val failure : Extlib.Pos.t -> ('a, unit, string, 'b) Stdlib.format4 -> 'c
val dim : t -> int