michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/init/nat): make \nat notation available at top level

Browse source
This commit is contained in:
Jeremy Avigad 2015-08-27 13:46:00 -04:00 committed by Leonardo de Moura
parent 51e0d31304
commit 840ef98829
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/data/int/div.lean
View file

@ -11,7 +11,6 @@ import data.int.order data.nat.div
open [coercions] [reduce-hints] nat open [coercions] [reduce-hints] nat
open [declarations] nat (succ) open [declarations] nat (succ)
open eq.ops open eq.ops
notation `ℕ` := nat
namespace int namespace int

3
library/init/nat.lean
View file

@ -7,8 +7,9 @@ prelude
import init.wf init.tactic init.num import init.wf init.tactic init.num
open eq.ops decidable or open eq.ops decidable or
notation `ℕ` := nat
namespace nat namespace nat
notation `ℕ` := nat
/- basic definitions on natural numbers -/ /- basic definitions on natural numbers -/
inductive le (a : ℕ) : ℕ → Prop := inductive le (a : ℕ) : ℕ → Prop :=