package lambdapi

  1. Overview
  2. Docs
package lambdapi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Export.DkSource

Export a Lambdapi signature to Dedukti.

Translation of identifiers. Lambdapi identifiers that are Dedukti keywords or invalid Dedukti identifiers are escaped, a feature offered by Dedukti.

Sourceval keyword_table : (string, Parsing.DkTokens.token) Hashtbl.t
Sourceval is_keyword : string -> bool
Sourceval is_ident : string -> bool
Sourceval is_mident : string -> bool
Sourceval ident : string Lplib.Base.pp

Translation of paths. Paths equal to the !current_path are not printed. Non-empty paths end with a dot. We assume that the module p1.p2.p3 is in the file p1_p2_p3.dk.

Sourceval path_elt : string Lplib.Base.pp
Sourceval current_path : string list ref
Sourceval qid : (Common.Path.t * string) Lplib.Base.pp
Sourcetype decl =
  1. | Sym of Core.Term.sym
  2. | Rule of Common.Path.t * string * Core.Term.rule

Type of Dedukti declarations.

Declarations are ordered wrt their positions in the source.

Sourceval pos_of_decl : decl -> Common.Pos.popt

Translation of terms.

Sourceval patt : string Lplib.Base.pp

Translation of declarations.

Sourceval modifiers : Core.Term.sym -> string list
Sourceval rule_decl : (Common.Path.t * string * Core.Term.rule) Lplib.Base.pp
Sourceval decls_of_sign : Core.Sign.t -> decl list

decls_of_sign sign computes a list of declarations for the signature sign, in order of appearance in the source.

Translation of a signature.

Sourceval require : Common.Path.t -> 'a -> unit
Sourceval sign : Core.Sign.t -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct