lambdapi 2.3.1 · OCaml Package

Translate the parser-level AST to Coq.

val log : 'a Lplib.Base.outfmt -> 'a

val stt : bool Stdlib.ref

val translate_ident : string -> string

val raw_ident : string Lplib.Base.pp

val ident : Parsing.Syntax.p_ident Lplib.Base.pp

val meta_ident : Parsing.Syntax.p_meta_ident Lplib.Base.pp

val param_id : Parsing.Syntax.p_ident option Lplib.Base.pp

val param_ids : Parsing.Syntax.p_ident option list Lplib.Base.pp

val raw_path : Common.Path.t Lplib.Base.pp

val path : Parsing.Syntax.p_path Lplib.Base.pp

val qident : Parsing.Syntax.p_qident Lplib.Base.pp

val modifier : Parsing.Syntax.p_modifier Lplib.Base.pp

val modifiers : Parsing.Syntax.p_modifier list Lplib.Base.pp

type priority = [

]

The possible priority levels are `Func (top level, including abstraction and product), `Appl (application) and `Atom (smallest priority).

val term : Parsing.Syntax.p_term Lplib.Base.pp

val params : Parsing.Syntax.p_params Lplib.Base.pp

val params_list : Parsing.Syntax.p_params list Lplib.Base.pp

val typ : Parsing.Syntax.p_term option Lplib.Base.pp

val rule : string -> Parsing.Syntax.p_rule Lplib.Base.pp

val inductive : string -> Parsing.Syntax.p_inductive Lplib.Base.pp

val proof_end : Parsing.Syntax.p_proof_end Lplib.Base.pp

val rw_patt : Parsing.Syntax.p_rw_patt Lplib.Base.pp

val tactic : Parsing.Syntax.p_tactic Lplib.Base.pp

val assoc : Pratter.associativity Lplib.Base.pp

val notation : string Core.Sign.notation Lplib.Base.pp

val subproof : Parsing.Syntax.p_subproof Lplib.Base.pp

val subproofs : Parsing.Syntax.p_subproof list Lplib.Base.pp

val proofsteps : Parsing.Syntax.p_subproof Lplib.Base.pp

val proofstep : Parsing.Syntax.p_proofstep Lplib.Base.pp

val proof : (Parsing.Syntax.p_proof * Parsing.Syntax.p_proof_end) Lplib.Base.pp

val command : Parsing.Syntax.p_command Lplib.Base.pp

val ast : Parsing.Syntax.ast Lplib.Base.pp

val print : bool -> Parsing.Syntax.ast -> unit

print b ast sets stt to b and translates ast to Coq on standard output.

package lambdapi