package dedukti

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type env_error =

val init : string -> Basic.mident

val get_name : unit -> Basic.mident

val get_type : 
  Basic.loc ->
  Basic.name ->
  (Term.term, Signature.signature_error) Basic.error

val get_dtree : 
  Basic.loc ->
  Basic.name ->
  ((int * Dtree.dtree) option, Signature.signature_error) Basic.error

val export : unit -> bool

val import : 
  Basic.loc ->
  Basic.mident ->
  (unit, Signature.signature_error) Basic.error

val declare : 
  Basic.loc ->
  Basic.ident ->
  Signature.staticity ->
  Term.term ->
  (unit, env_error) Basic.error

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 infer : 
  ?ctx:Term.typed_context ->
  Term.term ->
  (Term.term, env_error) Basic.error

val check : 
  ?ctx:Term.typed_context ->
  Term.term ->
  Term.term ->
  (unit, env_error) Basic.error

val reduction : 
  ?ctx:Term.typed_context ->
  ?red:Reduction.red_cfg ->
  Term.term ->
  (Term.term, 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