diff --git a/src/lnf.rs b/src/lnf.rs index f8b3ad9..9e38aea 100644 --- a/src/lnf.rs +++ b/src/lnf.rs @@ -31,7 +31,16 @@ impl TypeTerm { match self { TypeTerm::Ladder(args) => { for x in args.into_iter() { - new_ladder.push(x.normalize()); + match x.normalize() { + TypeTerm::Ladder(gs) => { + for g in gs { + new_ladder.push(g); + } + } + g => { + new_ladder.push(g); + } + } } } @@ -102,9 +111,7 @@ impl TypeTerm { TypeTerm::Ladder( v ) => { v }, - _ => { - unreachable!(); - } + flat => vec![ flat ] } } } diff --git a/src/test/subtype.rs b/src/test/subtype.rs index 836b492..54ad397 100644 --- a/src/test/subtype.rs +++ b/src/test/subtype.rs @@ -72,5 +72,26 @@ fn test_syntactic_subtype() { ), Err(None) ); + + assert_eq!( + dict.parse("~ℕ").expect("parse error") + .is_syntactic_subtype_of( + &dict.parse("ℕ").expect("parse errror") + ), + Ok(1) + ); + + assert_eq!( + dict.parse(" + +~ℕ +~ +~< Seq ~ Char >" + ).expect("parse error") + .is_syntactic_subtype_of( + &dict.parse("").expect("parse errror") + ), + Ok(4) + ); }