lambda_types/
boolean.rs

1use crate::{define, primitives};
2
3/// Truthy church boolean.
4pub type True = primitives::FirstOf;
5/// Falsy church boolean.
6pub type False = primitives::SecondOf;
7
8define! {
9    /// Boolean and operation. Takes two church booleans, and returns whether both are true.
10    /// ```text
11    /// λa.λb.aba
12    /// ```
13    pub fn And ::= {Lhs. Rhs. { Lhs, Rhs, Lhs }} where 
14        Lhs: Rhs,
15        {Lhs, Rhs}: Lhs;
16    /// Boolean or operation. Takes two church booleans, and returns whether either is true.
17    /// ```text
18    /// λa.λb.aab
19    /// ```
20    pub fn Or ::= {Lhs. Rhs. { Lhs, Lhs, Rhs }} where
21        Lhs: Lhs,
22        {Lhs, Lhs}: Rhs;
23    /// Boolean xor operation. Takes two church booleans, and returns whether only one is true.
24    /// ```text
25    /// N ::= Not
26    /// λa.λb.a(Nb)b
27    /// ```
28    pub fn Xor ::= {Lhs. Rhs. { Lhs, {Not, Rhs}, Rhs }} where
29        Not: Rhs,
30        Lhs: { Not, Rhs },
31        {Lhs, { Not, Rhs }}: Rhs;
32    /// Boolean not operation. Takes a church boolean and returns its inverse.
33    /// ```text
34    /// T ::= True
35    /// F ::= False
36    /// λv.vFT
37    /// ```
38    pub fn Not ::= {Value. { Value, False, True }} where
39        Value: False,
40        {Value, False}: True;
41    /// Alternation. Takes a church boolean and two values, and returns the first if the boolean is true, otherwise the second.
42    /// ```text
43    /// λp.λa.λb.pab
44    /// ```
45    pub fn If ::= {Predicate. Truthy. Falsy. { Predicate, Truthy, Falsy }} where
46        Predicate: Truthy,
47        {Predicate, Truthy}: Falsy;
48}
lambda_types/boolean.rs

lambda_types/
boolean.rs
