Function lambda_calculus::data::result::option_err
source · pub fn option_err() -> Term
Expand description
Applied to a lambda-encoded Result
it produces a lambda-encoded Option
containing the Err
value.
OPTION_ERR ≡ λa.a (λx.NONE) SOME ≡ λ 1 (λ NONE) SOME
Example
use lambda_calculus::data::result::option_err;
use lambda_calculus::data::option::none;
use lambda_calculus::*;
let ok_one: Result<usize, usize> = Ok(1);
let err_two: Result<usize, usize> = Err(2);
assert_eq!(beta(app(option_err(), ok_one.into_church()), NOR, 0), none());
assert_eq!(beta(app(option_err(), err_two.into_church()), NOR, 0), Some(2).into_church());