Module `Export.Coq`Source

Translate the parser-level AST to Coq.

There are two modes:

raw_coq mode (option -o raw_coq): translation of the AST as it is (lambdapi-calculus is a subset system of coq if we ignore rules)

stt_coq mode (option -o stt_coq): translation of the AST as an encoding in simple type theory.

The encoding can be specified through a lambdapi file (option --encoding).

In both modes, a renaming map can be provided to rename some identifiers.

The renaming map can be specified through a lambdapi file (option --renaming).

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

Symbols necessary to encode STT.

Sourcetype builtin =

| Set
| Prop
| Arr
| El
| Imp
| All
| Prf
| Eq
| Or
| And
| Ex
| Not

Sourceval index_of_builtin : builtin -> int

Sourceval nb_builtins : int

Sourceval builtin_of_index : int -> builtin

Sourceval index_of_name : string -> int option

Sourceval name_of_index : int -> string

Sourceval builtin : Core.Term.qident array

Sourceval sym : builtin -> Core.Term.qident

Set renaming map from file.

Sourceval rmap : Lplib.Extra.StrMap.key Lplib.Extra.StrMap.t ref

Sourceval set_renaming : string -> unit

Set symbols whose declarations have to be erased.

Sourceval erase : Lplib.Extra.StrSet.t ref

Sourcemodule Qid : sig ... end

Sourcemodule QidMap : sig ... end

Sourceval map_erased_qid_coq : string QidMap.t ref

Sourceval set_erasing : string -> unit

Set encoding.

Sourceval map_qid_builtin : builtin QidMap.t ref

Sourceval set_encoding : string -> unit

Translation of identifiers.

Sourceval translate_ident : string -> string

Sourceval raw_ident : string Lplib.Base.pp

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

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

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

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

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

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

Translation of terms.

Sourceval stt : bool ref

Sourceval use_implicits : bool ref

Sourceval use_notations : bool ref

Source

val p_get_args : 
  Parsing.Syntax.p_term ->
  Parsing.Syntax.p_term * Parsing.Syntax.p_term list

Source

val app : 
  Parsing.Syntax.p_term ->
  (Parsing.Syntax.p_term -> Parsing.Syntax.p_term list -> 'a) ->
  (Parsing.Syntax.p_term ->
    Parsing.Syntax.p_term list ->
    bool ->
    builtin ->
    'a) ->
  'a

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

Source

val arrow : 
  Format.formatter ->
  Parsing.Syntax.p_term ->
  Parsing.Syntax.p_term ->
  unit

Source

val abst : 
  Format.formatter ->
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term ->
  unit

Source

val prod : 
  Format.formatter ->
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term ->
  unit

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

Sourceval raw_params : Parsing.Syntax.p_params Lplib.Base.pp

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

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

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

Sourceval typopt : Parsing.Syntax.p_term option Lplib.Base.pp

Translation of commands.

Sourceval is_lem : Parsing.Syntax.p_modifier_aux Common.Pos.loc -> bool

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

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

Set Coq required file.

Sourceval require : string option ref

Sourceval set_requiring : string -> unit

Sourceval print : Parsing.Syntax.ast -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/lambdapi.export/Export/Coq/index.html

Module `Export.Coq`Source

package lambdapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/lambdapi.export/Export/Coq/index.html

Module Export.CoqSource

Module `Export.Coq`Source