change type of Tactic.#have (Deducteam#40)

Author: fblanqui

Eq.lp

@@ -7,13 +7,16 @@ constant symbol = [a] : τ a → τ a → Prop;
 notation = infix 10;
 
 constant symbol eq_refl [a] (x:τ a) : π (x = x);
-constant symbol ind_eq [a] [x y:τ a] : π (x = y) → Π p, π (p y) → π (p x);
+
+symbol ind_eq [a] [x y:τ a] : π (x = y) → Π p, π (p y) → π (p x);
 
 builtin "eq"    ≔ =;
 builtin "refl"  ≔ eq_refl;
 builtin "eqind" ≔ ind_eq;
 
-symbol ≠ [a] (x y : τ a) ≔ ¬ (x = y); notation ≠ infix 10; // \neq
+symbol ≠ [a] (x y : τ a) ≔ ¬ (x = y);
+
+notation ≠ infix 10; // \neq
 
 opaque symbol feq [a b] (f:τ a → τ b) [x x':τ a] : π(x = x') → π(f x = f x') ≔
 begin

Nat.lp

@@ -614,7 +614,7 @@ begin
   };
 end;
 
-// order on ℕ
+// Boolean ordering functions
 
 symbol ≤ : ℕ → ℕ → 𝔹; notation ≤ infix left 10;
 

Tactic.lp

@@ -26,7 +26,7 @@ builtin "fail" ≔ #fail;
 constant symbol #generalize : Π [a], τ a → Tactic;
 builtin "generalize" ≔ #generalize;
 
-constant symbol #have : String → Π p, π p → Tactic;
+constant symbol #have : String → Prop → Tactic;
 builtin "have" ≔ #have;
 
 constant symbol #induction : Tactic;

Z.lp

@@ -232,6 +232,7 @@ end;
 // Negation
 
 symbol - x y ≔ x + — y;
+
 notation - infix left 20;
 
 symbol -_same z : π (z + — z = Z0) ≔
@@ -507,10 +508,10 @@ end;
 
 // Directional comparison operators
 
-symbol ≤ x y ≔ ¬ (istrue(isGt (x ≐ y)));
+symbol ≤ x y ≔ ¬ (istrue(isGt(x ≐ y)));
 notation ≤ infix 10;
 
-symbol < x y ≔ istrue(isLt (x ≐ y));
+symbol < x y ≔ istrue(isLt(x ≐ y));
 notation < infix 10;
 
 symbol ≥ x y ≔ ¬ (x < y);