Module functions 

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

Functions

conjunction_intro

Construct a proof of P ∧ Q from individual proofs.

existential_witness

Pack a witness value with a proof to produce a proof of ∃x.P(x).

extract_program

Attempt to extract a computational program from a constructive proof.

is_constructive

Check whether a proposition is fully constructive (intuitionistically valid).

modus_ponens_extract

Extract a conclusion from modus ponens: given a proof of P and a proof of P → Q, produce a proof of Q.

proof_to_rust

Generate a Rust pseudocode string representing the extracted program.

realizability_check

Check whether a proposition has a realizer — i.e., there exists a computable function that extracts a witness from any proof of the proposition.

simplify_proof_term

Perform beta/eta reduction on a proof term, returning a simplified equivalent.

type_check_proof

Verify that a proof term is well-typed with respect to a proposition.