deducteam / lambdapi-logics Goto Github PK

Hi,

In TFF/Nat.lp the symbol ∨: ℕ → ℕ → ℕ; is defined but it seems to produce a conflict with the disjunction defined in TFF/Prop.lp : constant symbol ∨ : Prop → Prop → Prop;

For example, if I load the Nat.lp file then the following definition is not accepted anymore:
constant symbol MyT : TYPE;

constant symbol r : MyT → Prop;
constant symbol p : MyT → Prop;
constant symbol q : MyT → Prop;
constant symbol ax1 x : π( r x ⇒ p x ∨ q x);
It assumes ∨: ℕ → ℕ → ℕ instead of ∨ : Prop → Prop → Prop;

Am i missing something ?

I do not know if it is a bug in lambdapi, the priorities that have to be changed, or just the definition of the connectives that needs to be parenthesized, but the definitions of the classical connectives are badly parsed

require open Logic.U.Prop Logic.U.Classic;

symbol p : Prop;
symbol q : Prop;

assertnot  ⊢ p ∧ᶜ q ≡ (¬ ¬ p) ∧ (¬ ¬ q); 
assert ⊢ p ∧ᶜ q ≡ ¬ ¬ (p ∧ (¬ ¬ q));

and the same for ∨ᶜ.