oxilean_std/program_extraction/mod.rs
1//! Program extraction from constructive proofs via the Curry-Howard correspondence.
2//!
3//! This module implements the computational content extraction from intuitionistic
4//! proofs. Under the Curry-Howard isomorphism, propositions correspond to types
5//! and proofs correspond to programs; this module makes that extraction explicit.
6
7pub mod functions;
8pub mod types;
9
10pub use functions::*;
11pub use types::*;