Skip to main content

MATH_BOOL

logicaffeine_web::ui::examples

Constant MATH_BOOL 

Source 
pub const MATH_BOOL: &str = r#"Inductive MyBool := Yes : MyBool | No : MyBool.

Check Yes.
Check No.
Eval Yes.
Eval No.

Definition id_bool : MyBool -> MyBool := fun b : MyBool => b.

Check id_bool.
Eval id_bool Yes.
Eval id_bool No.
"#;