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 { 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.")?;