refactor(library/init): move more library files to new elaborator

library/init/bool.lean

@@ -3,23 +3,30 @@
 -- Author: Leonardo de Moura
 prelude
 import init.datatypes
+set_option new_elaborator true
 
 namespace bool
   attribute [inline]
-  definition cond {A : Type} (b : bool) (t e : A) :=
-  bool.rec_on b e t
+  definition cond {A : Type} : bool → A → A → A
+  | tt a b := a
+  | ff a b := b
 
   attribute [inline]
-  definition bor (a b : bool) :=
-  bool.rec_on a (bool.rec_on b ff tt) tt
+  definition bor : bool → bool → bool
+  | tt _  := tt
+  | ff tt := tt
+  | ff ff := ff
 
   attribute [inline]
-  definition band (a b : bool) :=
-  bool.rec_on a ff (bool.rec_on b ff tt)
+  definition band : bool → bool → bool
+  | ff _  := ff
+  | tt ff := ff
+  | tt tt := tt
 
   attribute [inline]
-  definition bnot (a : bool) :=
-  bool.rec_on a tt ff
+  definition bnot : bool → bool
+  | tt := ff
+  | ff := tt
 end bool
 
 notation a || b := bool.bor a b

library/init/ordering.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.to_string init.prod init.sum
+set_option new_elaborator true
 
 inductive ordering
 | lt | eq | gt
@@ -19,9 +20,9 @@ structure [class] has_ordering (A : Type) :=
 (cmp : A → A → ordering)
 
 definition nat.cmp (a b : nat) : ordering :=
-if a < b      then lt
-else if a = b then eq
-else               gt
+if a < b      then ordering.lt
+else if a = b then ordering.eq
+else               ordering.gt
 
 attribute [instance]
 definition nat_has_ordering : has_ordering nat :=

library/init/relation.lean

@@ -7,6 +7,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.logic
+set_option new_elaborator true
 
 -- TODO(Leo): remove duplication between this file and algebra/relation.lean
 -- We need some of the following definitions asap when "initializing" Lean.

library/init/sum.lean

@@ -7,6 +7,7 @@ The sum type, aka disjoint union.
 -/
 prelude
 import init.logic
+set_option new_elaborator true
 
 notation A ⊕ B := sum A B
 variables {A B : Type}

library/init/timeit.lean

@@ -3,6 +3,7 @@
 -- Author: Leonardo de Moura
 prelude
 import init.string
+set_option new_elaborator true
 
 /- This function has a native implementation that tracks time. -/
 definition timeit {A : Type} (s : string) (f : unit → A) : A :=

library/init/to_string.lean

@@ -3,6 +3,7 @@
 -- Author: Leonardo de Moura
 prelude
 import init.string init.bool init.subtype init.unsigned init.prod init.sum
+set_option new_elaborator true
 open bool list sum prod sigma subtype nat
 
 structure [class] has_to_string (A : Type) :=
@@ -17,7 +18,8 @@ has_to_string.mk (λ b, cond b "tt" "ff")
 
 attribute [instance]
 definition decidable.has_to_string {p : Prop} : has_to_string (decidable p) :=
-has_to_string.mk (λ b, if p then "tt" else "ff")
+-- Remark: type class inference will not consider local instance `b` in the new elaborator
+has_to_string.mk (λ b : decidable p, @ite p b _ "tt" "ff")
 
 definition list.to_string_aux {A : Type} [has_to_string A] : bool → list A → string
 | b  []      := ""

library/init/trace.lean

@@ -3,6 +3,7 @@
 -- Author: Leonardo de Moura
 prelude
 import init.string
+set_option new_elaborator true
 
 /- This function has a native implementation that displays the given string in the regular output stream. -/
 definition trace {A : Type} (s : string) (f : unit → A) : A :=

library/init/unit.lean

@@ -5,6 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.logic
+set_option new_elaborator true
 
 theorem unit_eq (a b : unit) : a = b :=
 unit.rec_on a (unit.rec_on b rfl)