From 2189e495ddec4f333f4f6956bba336fb2e598659 Mon Sep 17 00:00:00 2001
From: nilfit <nils.fitinghoff@gmail.com>
Date: Tue, 18 Sep 2018 12:59:45 +0200
Subject: [PATCH] remove redundant `import`s and uncomment a useful `use`
---
peano_nat.mlw | 14 +++++++-------
1 file changed, 7 insertions(+), 7 deletions(-)
diff --git a/peano_nat.mlw b/peano_nat.mlw
index cae2d2d..6690f3b 100644
--- a/peano_nat.mlw
+++ b/peano_nat.mlw
@@ -48,7 +48,7 @@ end
module Add
- use import Nat
+ use Nat
goal plus_ol:
forall n. O + n = n
@@ -107,9 +107,9 @@ end
module Compare
- use import Nat
- (* use import Add *)
- (* use import Inconsistency *)
+ use Nat
+ use Add
+ (* use Inconsistency *)
inductive le nat nat =
| Le_n : forall n:nat. le n n
@@ -132,8 +132,8 @@ end
module Sub
- use import Nat
- use import Compare
+ use Nat
+ use Compare
function sub (n m:nat) : nat =
match n, m with
@@ -173,4 +173,4 @@ module Sub
lemma sub_lt_nm:forall n m. ... -> sub n m < n
*)
-end
\ No newline at end of file
+end
--
GitLab