Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
The signature which implements a reification function.
val md : Kernel.Basic.midentmodule name of the encoding
val entries : unit -> Parsers.Entry.entry listList of declarations
val signature : Kernel.Signature.tSignature of the encoding. Redudant with entries
val encode_term :
?sg:Kernel.Signature.t ->
?ctx:Kernel.Term.typed_context ->
Kernel.Term.term ->
Kernel.Term.termencode_term sg ctx t encodes a term t. sg and ctx are used only if safe is true
val decode_term : Kernel.Term.term -> Kernel.Term.termdecode_term t decodes a term t
val encode_rule :
?sg:Kernel.Signature.t ->
'a Kernel.Rule.rule ->
'a Kernel.Rule.ruleencode_rule sg r encodes a rule r. sg is used only if safe is true