use lambda_calculus::{
parse,
parser::ParseError,
term::Notation::{Classic, DeBruijn},
};
#[test]
fn parse_debruijn_and_classic() -> Result<(), ParseError> {
for (dbr, cla) in [
("12", "a b"),
("λλ21", "λs. λz. s z"),
(
"λ2134(λ3215(λ4321)3215)2134",
"λx. w x y z (λy. w x y z (λz. w x y z) w x y z) w x y z",
),
(
"λ2(λ421(5(λ4127)λ8))67",
"λx. a (λt. b x t (f (λu. a u t z) λs. w)) w y",
),
(
"(λλλλ42(321))(λλ1)(λλ21)12",
"(λm.λn.λs.λz. m s (n s z)) (λs.λz. z) (λs.λz. s z) s z",
),
] {
let term_dbr = parse(dbr, DeBruijn)?;
let term_cla = parse(cla, Classic)?;
assert_eq!(term_dbr, term_cla);
}
Ok(())
}