package lambdapi

  1. Overview
  2. Docs
module Command : sig ... end

Handling of commands.

module Compile : sig ... end

High-level compilation functions.

module Inductive : sig ... end

Generation of induction principles.

module Proof : sig ... end

Proofs and tactics.

module Query : sig ... end

Handling of queries.

module Rewrite : sig ... end

Implementation of the rewrite tactic.

module Tactic : sig ... end

Handling of tactics.

module Why3_tactic : sig ... end

Calling a prover using Why3.

OCaml

Innovation. Community. Security.