Module `Export.Rawdk`Source

Translate the parser-level AST to Dedukti.

Sourceval raw_ident : string Lplib.Base.pp

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

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

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

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

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

Source

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

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

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

Source

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

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

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

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

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

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

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

Sourceval bool : bool Lplib.Base.pp

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

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

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

Source

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

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

Source

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

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

Source

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

Source

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

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

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

Sourceval print : Parsing.Syntax.ast -> unit

package lambdapi

Module Export.RawdkSource

Module `Export.Rawdk`Source