Skip to main content

is_constructive

oxilean_std::program_extraction::functions

Function is_constructive 

Source 
pub fn is_constructive(prop: &ConstructiveProp) -> bool
Expand description

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

A proposition is constructive if it avoids the law of excluded middle and double-negation elimination at top level, and all subpropositions are also constructive.