lambdapi 2.5.1 · OCaml Package

Translate the parser-level AST to Dedukti.

val raw_ident : string Lplib.Base.pp

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

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

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

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

val let_typ : 
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term Lplib.Base.pp

val let_dfn : 
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term Lplib.Base.pp

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

val terms : Parsing.Syntax.p_term array Lplib.Base.pp

val param : 
  Parsing.Syntax.p_term option ->
  string ->
  Parsing.Syntax.p_ident option Lplib.Base.pp

val params : string -> Parsing.Syntax.p_params Lplib.Base.pp

val params_list : string -> Parsing.Syntax.p_params list Lplib.Base.pp

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

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

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

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

val bool : bool Lplib.Base.pp

val assertion : (bool * Parsing.Syntax.p_assertion) Lplib.Base.pp

val strat : Core.Eval.strat Lplib.Base.pp

val query : Parsing.Syntax.p_query Lplib.Base.pp

val remove_wraps : 
  Parsing.Syntax.p_term_aux Common.Pos.loc ->
  Parsing.Syntax.p_term_aux Common.Pos.loc

val rule : Parsing.Syntax.p_rule Lplib.Base.pp

type modifiers =
  Core.Term.prop list
  * Core.Term.expo list
  * Core.Term.match_strat list
  * Parsing.Syntax.p_modifier_aux list

val partition_modifiers : Parsing.Syntax.p_modifier list -> modifiers

val modifiers : 
  Parsing.Syntax.p_term option ->
  Parsing.Syntax.p_modifier list Lplib.Base.pp

val get_ac_typ : 
  Common.Pos.popt ->
  modifiers ->
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term option ->
  Parsing.Syntax.p_term option

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

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

val print : Parsing.Syntax.ast -> unit

package lambdapi