Skip to content
Snippets Groups Projects
Commit 2189e495 authored by nilfit's avatar nilfit
Browse files

remove redundant `import`s and uncomment a useful `use`

parent d259aaa2
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 7 additions and 7 deletions
peano_nat.mlw
+ 7
− 7
View file @ 2189e495
...@@ -48,7 +48,7 @@ end ...@@ -48,7 +48,7 @@ end
module Add module Add
use import Nat use Nat
goal plus_ol: goal plus_ol:
forall n. O + n = n forall n. O + n = n
...@@ -107,9 +107,9 @@ end ...@@ -107,9 +107,9 @@ end
module Compare module Compare
use import Nat use Nat
(* use import Add *) use Add
(* use import Inconsistency *) (* use Inconsistency *)
inductive le nat nat = inductive le nat nat =
| Le_n : forall n:nat. le n n | Le_n : forall n:nat. le n n
...@@ -132,8 +132,8 @@ end ...@@ -132,8 +132,8 @@ end
module Sub module Sub
use import Nat use Nat
use import Compare use Compare
function sub (n m:nat) : nat = function sub (n m:nat) : nat =
match n, m with match n, m with
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment