sig
val check_tau : Lang.tau -> bool
val check_term : Lang.F.term -> bool
class type engine =
object
method callstyle : Qed.Engine.callstyle
method pp_atom : Stdlib.Format.formatter -> Lang.F.term -> unit
method pp_flow : Stdlib.Format.formatter -> Lang.F.term -> unit
end
val f_nil : Lang.Fun.t
val f_elt : Lang.Fun.t
val f_nth : Lang.Fun.t
val f_cons : Lang.Fun.t
val f_concat : Lang.Fun.t
val f_repeat : Lang.Fun.t
val export :
#Vlist.engine -> Stdlib.Format.formatter -> Lang.F.term list -> unit
val pretty :
#Vlist.engine -> Stdlib.Format.formatter -> Lang.F.term list -> unit
val elements :
#Vlist.engine -> Stdlib.Format.formatter -> Lang.F.term list -> unit
val pprepeat :
#Vlist.engine -> Stdlib.Format.formatter -> Lang.F.term list -> unit
val shareable : Lang.F.term -> bool
end