Skip to content

Commit e5239f3

Browse files
committed
fix: addtwo function now adds two
1 parent c3ad007 commit e5239f3

1 file changed

Lines changed: 27 additions & 1 deletion

File tree

src/experiments/magic_test_function.rs

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ pub fn coadd() -> Term {
4141
}
4242

4343
pub fn addtwo() -> Term {
44-
let mut comp = app!(succ(), succ());
44+
let mut comp = abs!(1, app!(succ(), app!(succ(), Var(1))));
4545
comp.reduce(HAP, 0);
4646
comp
4747
}
@@ -366,3 +366,29 @@ pub fn succ_search_with_test() {
366366
dump_series_to_file(fname, &series, &[id]).expect("Cannot write to file");
367367
}
368368
}
369+
370+
mod tests {
371+
use lambda_calculus::{
372+
app, data::boolean::tru, data::num::church::add, reduction::Order::HNO, IntoChurchNum,
373+
};
374+
375+
use crate::experiments::magic_test_function::{addtwo, test_addtwo, test_succ};
376+
377+
use super::test_add;
378+
379+
#[test]
380+
fn add_test_reduces() {
381+
let add_test = test_add(3, 4);
382+
let mut comp = app!(add_test, add());
383+
comp.reduce(HNO, 0);
384+
assert!(comp.is_isomorphic_to(&tru()))
385+
}
386+
387+
#[test]
388+
fn addtwo_test_reduces() {
389+
let add_test = test_addtwo(3);
390+
let mut comp = app!(add_test, addtwo());
391+
comp.reduce(HNO, 0);
392+
assert!(comp.is_isomorphic_to(&tru()))
393+
}
394+
}

0 commit comments

Comments
 (0)