From 3c84054e8c9705b9d51f722e8b1aaa532c8d9f8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Michael=20F=C3=A4rber?= <michael.faerber@gedenkt.at>
Date: Wed, 24 Apr 2024 19:54:32 +0200
Subject: [PATCH] Test variable contexts for declarations.

---
 dedukti-parse/src/lib.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/dedukti-parse/src/lib.rs b/dedukti-parse/src/lib.rs
index 7d0152e..eeac03d 100644
--- 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.")?;