dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Env
type env_error =
| EnvErrorType of Typing.typing_error
| EnvErrorSignature of Signature.signature_error
| KindLevelDefinition of Basic.loc * Basic.ident
val init : string -> Basic.mident
val get_name : unit -> Basic.mident
val get_dtree : Basic.loc -> Basic.name -> ( (int * Dtree.dtree) option, Signature.signature_error ) Basic.error
val export : unit -> bool
val define : Basic.loc -> Basic.ident -> Term.term -> Term.term option -> ( unit, env_error ) Basic.error
val define_op : Basic.loc -> Basic.ident -> Term.term -> Term.term option -> ( unit, env_error ) Basic.error
val add_rules : Rule.untyped_rule list -> ( Rule.typed_rule list, env_error ) Basic.error
val check : ?ctx:Term.typed_context -> Term.term -> Term.term -> ( unit, env_error ) Basic.error
val are_convertible : ?ctx:Term.typed_context -> Term.term -> Term.term -> ( bool, env_error ) Basic.error
val unsafe_reduction : ?red:Reduction.red_cfg -> Term.term -> Term.term