oxilean-std 0.1.2

OxiLean standard library
Documentation 
1
2
3
4
5
6
7
8
9
10
11

//! 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.

pub mod functions;
pub mod types;

pub use functions::*;
pub use types::*;