1use crate::{ops::Or, term::{Term, ValueEq}};
2
3use super::{False, True};
4
5pub fn or_false_eq_a<A: Term<Type = bool>>(
6) -> ValueEq<Or<A, False>, A>
7{
8 unsafe {ValueEq::axiom()}
9}
10
11pub fn or_true_eq_true<A: Term<Type = bool>>(
12) -> ValueEq<Or<A, True>, True>
13{
14 unsafe {ValueEq::axiom()}
15}
16
17pub fn or_commutative<A: Term<Type = bool>, B: Term<Type = bool>>(
18) -> ValueEq<Or<A, B>, Or<B, A>>
19{
20 unsafe {ValueEq::axiom()}
21}
22
23pub fn or_a_a_eq_a<A: Term<Type = bool>>(
24) -> ValueEq<Or<A, A>, A>
25{
26 unsafe {ValueEq::axiom()}
27}
28
29pub fn false_or_eq_b<B: Term<Type = bool>>(
30) -> ValueEq<Or<False, B>, B>
31{
32 or_commutative() + or_false_eq_a()
33}
34
35pub fn true_or_eq_true<B: Term<Type = bool>>(
36) -> ValueEq<Or<True, B>, True>
37{
38 or_commutative() + or_true_eq_true()
39}