lambda_types/
datatypes.rs

1
2
3use crate::{
4    primitives::Constant,
5    boolean::{True, False},
6    define
7};
8
9define! {
10    /// Pair of two values.
11    /// ```text
12    /// λx.λy.λf.fxy
13    /// ```
14    pub fn Pair ::= { X. Y. F. { F, X, Y }} where
15        F: X,
16        {F, X}: Y;
17    /// Gets the first element of a pair.
18    /// ```text
19    /// T ::= True
20    /// λp.pT
21    /// ```
22    pub fn First ::= { P. { P, True }} where P: True;
23    /// Gets the second element of a pair.
24    /// ```text
25    /// F ::= False
26    /// λp.pF
27    /// ```
28    pub fn Second ::= { P. { P, False }} where P: False;
29    /// Tests whether a value is [`Nil`].
30    /// ```text
31    /// F ::= False
32    /// λp.p(λx.λy.F)
33    /// ```
34    pub fn Null ::= { P. { P, Constant<Constant<False>> }} where P: (Constant<Constant<False>>);
35}
36
37/// An empty singly linked list.
38pub type Nil = Constant<True>;
39
40#[test]
41fn t() {
42    use crate::prelude::*;
43
44    let _: call!{ Null, Nil } = True::default();
45    let _: call!{ Null, {Pair, (), Nil} } = False::default();
46}
lambda_types/datatypes.rs

lambda_types/
datatypes.rs
