Module program_extraction 

Program extraction from constructive proofs via the Curry-Howard correspondence.

This module implements the computational content extraction from intuitionistic proofs. Under the Curry-Howard isomorphism, propositions correspond to types and proofs correspond to programs; this module makes that extraction explicit.

Re-exports

pub use functions::*;

pub use types::*;

Modules

functions

Functions for program extraction from constructive proofs via the Curry-Howard correspondence.

types

Types for program extraction from constructive proofs (Curry-Howard correspondence).