1. Overview
  2. Docs

Deduki backend for proofs

Work in progress...

module type S = Backend_intf.S
module type Arg = sig ... end
module Make (S : Msat.S) (A : Arg with type formula := S.formula and type lemma := S.lemma and type proof := S.proof) : S with type t := S.proof

Functor to generate a backend to output proofs for the dedukti type checker.