test: reduce a classic notation

ljedrz · Aug 9, 2023 · 57fc702 · 57fc702
1 parent a93f443
commit 57fc702
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/tests/reduction.rs b/tests/reduction.rs
@@ -1,6 +1,7 @@
 extern crate lambda_calculus as lambda;
 
 use lambda::combinators::{I, O};
+use lambda::parser::ParseError;
 use lambda::*;
 use std::thread;
 
@@ -48,6 +49,20 @@ fn reduction_cbv() {
     assert_eq!(expr, I());
 }
 
+#[test]
+fn reduction_zero_plus_one() -> Result<(), ParseError> {
+    let mut expr = parse(
+        "(λm.λn.λs.λz. m s (n s z)) (λs.λz. z) (λs.λz. s z) s z",
+        Classic,
+    )?;
+    expr.reduce(CBV, 2);
+    assert_eq!(expr, parse("(λλ(λλ1)2((λλ21)21))9A", DeBruijn)?);
+    expr.reduce(CBV, 6);
+    assert_eq!(expr, parse("9A", DeBruijn)?);
+    assert_eq!(expr.to_string(), "i j");
+    Ok(())
+}
+
 #[test]
 #[ignore]
 fn reduction_huge() {