refactor(library): redefine string and char

library/data/list/basic.lean

@@ -8,10 +8,6 @@ Basic properties of lists.
 import logic tools.helper_tactics data.nat.order data.nat.sub
 open eq.ops nat prod function option
 
-inductive list (T : Type) : Type :=
-| nil {} : list T
-| cons   : T → list T → list T
-
 protected definition list.is_inhabited [instance] (A : Type) : inhabited (list A) :=
 inhabited.mk list.nil
 

library/init/char.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.fin
+open nat
+
+definition char := fin 256
+
+definition char.of_nat (n : nat) : char :=
+if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial

library/init/datatypes.lean

@@ -101,17 +101,14 @@ inductive bool : Type :=
 | ff : bool
 | tt : bool
 
-inductive char : Type :=
-mk : bool → bool → bool → bool → bool → bool → bool → bool → char
-
-inductive string : Type :=
-| empty : string
-| str   : char → string → string
-
 inductive option (A : Type) : Type :=
 | none {} : option A
 | some    : A → option A
 
+inductive list (T : Type) : Type :=
+| nil {} : list T
+| cons   : T → list T → list T
+
 -- Remark: we manually generate the nat.rec_on, nat.induction_on, nat.cases_on and nat.no_confusion.
 -- We do that because we want 0 instead of nat.zero in these eliminators.
 set_option inductive.rec_on   false

library/init/default.lean

@@ -8,4 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
-import init.monad
+import init.monad init.fin init.char init.string

library/init/fin.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.nat
+open nat
+
+structure fin (n : nat) := (val : nat) (is_lt : val < n)
+
+namespace fin
+
+attribute fin.val [coercion]
+
+variable {n : nat}
+
+lemma eq_of_veq : ∀ {i j : fin n}, (val i) = j → i = j
+| (mk iv ilt) (mk jv jlt) := assume (veq : iv = jv), sorry -- begin congruence, assumption end
+
+lemma veq_of_eq : ∀ {i j : fin n}, i = j → (val i) = j
+| (mk iv ilt) (mk jv jlt) := assume Peq,
+  show iv = jv, from fin.no_confusion Peq (λ Pe Pqe, Pe)
+
+lemma eq_iff_veq {i j : fin n} : (val i) = j ↔ i = j :=
+iff.intro eq_of_veq veq_of_eq
+
+end fin
+
+open decidable fin
+
+protected definition fin.has_decidable_eq [instance] (n : nat) : ∀ (i j : fin n), decidable (i = j)
+| (mk ival ilt) (mk jval jlt) :=
+  decidable_of_decidable_of_iff (nat.has_decidable_eq ival jval) eq_iff_veq

library/init/string.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.char
+
+definition string := list char
+
+definition string.empty : string := list.nil
+definition string.str : char → string → string := list.cons

library/init/tactic.lean

@@ -85,7 +85,7 @@ definition exact      (e : expr)         : tactic := builtin
 -- Relaxed version of exact that does not enforce goal type
 definition rexact     (e : expr)         : tactic := builtin
 definition check_expr (e : expr)         : tactic := builtin
-definition trace      (s : string)       : tactic := builtin
+-- definition trace      (s : string)       : tactic := builtin
 
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.