Test variable contexts for declarations.

01mf02 · Apr 24, 2024 · 3c84054 · 3c84054
1 parent 87faf8a
commit 3c84054
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/dedukti-parse/src/lib.rs b/dedukti-parse/src/lib.rs
@@ -330,6 +330,7 @@ impl Scoped<String> {
 fn positive() -> Result<(), Error> {
     Command::parse_str("prop : Type.")?;
     Command::parse_str("imp: prop -> prop -> prop.")?;
+    Command::parse_str("imp (l: prop) (r: prop): prop.")?;
     Command::parse_str("def prf: prop -> Type.")?;
     Command::parse_str("def f (x: A) : A.")?;
     Command::parse_str("def f (x: A) := t.")?;