package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
val qiden : Common.Path.t -> string -> p_term

qiden p s builds a P_Iden "@p.s".

val iden : string -> p_term

iden s builds a P_Iden "@s".

val var : Core.Term.tvar -> p_term

var v builds a P_Iden from Bindlib.name_of v.

val patt : string -> p_term array option -> p_term

patt s ts builds a P_Patt "$sts".

val patt0 : string -> p_term

patt0 s builds a P_Patt "$s".

val appl : p_term -> p_term -> p_term

appl t u builds P_Appl(t, u).

val appl_list : p_term -> p_term list -> p_term

appl_list t ts iterates appl.

wild builds a P_Wild.

val appl_wild : p_term -> int -> p_term

appl_wild t n applies t to n underscores.

val abst : p_ident option -> p_term -> p_term

abst idopt t builds a P_Abst over t.

val abst_list : p_ident option list -> p_term -> p_term

abst_list iterates abst.

val rule : p_term -> p_term -> p_rule