From affff63da5f20b31d1f77db705c0d88323421eea Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Sun, 17 May 2020 17:09:10 +0200
Subject: [PATCH] syntax and commenting invalid line

---
 paper/rat.lp       |  2 +-
 prelude/numbers.lp | 10 +++++-----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/paper/rat.lp b/paper/rat.lp
index c0a20bf..a64cde3 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -79,7 +79,7 @@ proof
   refine snd (Snz n)
   assume n Hn
   refine nznat_induction
-           (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n,Hn] ?zSnz[n,Hn]
+           (λz, (Z =ℕ (fst (Snz n) * (fst z))) ⊃ false) ?zOnz[n;Hn] ?zSnz[n;Hn]
   simpl
   refine snd (Snz n)
   assume m Hm
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index 28d32a6..d0ead4e 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -49,15 +49,15 @@ symbol associative_add
 constant symbol real_pred: η (pred numfield)
 definition real ≔ psub real_pred
 
-set flag "print_implicits" on
 symbol Num_real: ε (∀ (λx: η {|!Number!|}, real_pred (insertnum x)))
 
 // Built in the PVS typechecker
 
-definition nonzero_real ≔
-  psub {real}
-       (λx: η real,
-        neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
+// TODO: metavariables left
+// definition nonzero_real ≔
+//   psub {real}
+//        (λx: η real,
+//         neq {_} x (cast {_} {real} (λx, x) (insertnum 0) _))
 
 // symbol closed_plus_real: Π(x y: Term real),
 //   let pr ≔ S.restr numfield real_pred in
-- 
GitLab