feat(library/init/core): allow lists of proofs

library/init/core.lean

@@ -334,14 +334,14 @@ def decidable_rel {α : Sort u} (r : α → α → Prop) :=
 def decidable_eq (α : Sort u) :=
 decidable_rel (@eq α)
 
-inductive option (α : Type u)
+inductive option (α : Sort u)
 | none : option
 | some (val : α) : option
 
 export option (none some)
 export bool (ff tt)
 
-inductive list (T : Type u)
+inductive list (T : Sort u)
 | nil : list
 | cons (hd : T) (tl : list) : list
 

library/init/data/list/lemmas.lean

@@ -8,7 +8,7 @@ import init.data.list.basic init.function init.meta init.data.nat.lemmas
 import init.meta.interactive init.meta.smt.rsimp
 
 universes u v w w₁ w₂
-variables {α : Type u} {β : Type v} {γ : Type w}
+variables {α : Sort u} {β : Sort v} {γ : Sort w}
 
 namespace list
 open nat

library/init/meta/has_reflect.lean

@@ -47,9 +47,18 @@ meta instance name.reflect : has_reflect name
 | (name.mk_string  s n) := `(λ n, name.mk_string  s n).subst (name.reflect n)
 | (name.mk_numeral i n) := `(λ n, name.mk_numeral i n).subst (name.reflect n)
 
+meta instance list.reflect' {α : Sort} [has_reflect α] [reflected α] : has_reflect (list α)
+| []     := `([])
+| (h::t) := `(λ t, h :: t).subst (list.reflect' t)
+
 meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (list α)
 | []     := `([])
 | (h::t) := `(λ t, h :: t).subst (list.reflect t)
 
+-- `has_reflect_derive_handler` only generates this for `Sort`
+meta instance option.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (option α)
+| none     := `(none)
+| (some x) := `(some x)
+
 meta instance punit.reflect : has_reflect punit
 | () := `(_)

library/init/meta/interactive.lean

@@ -1206,7 +1206,8 @@ do (hs, gex, hex, all_hyps) ← decode_simp_arg_list_with_symm hs,
    when (all_hyps ∧ at_star ∧ not hex.empty) $ fail "A tactic of the form `simp [*, -h] at *` is currently not supported",
    s      ← join_user_simp_lemmas no_dflt attr_names,
    -- Erase `h` from the default simp set for calls of the form `simp [←h]`.
-   let to_erase := hs.foldl (λ l h, match h with
+   let to_erase : list name :=
+                   hs.foldl (λ l h, match h with
                                     | (const id _, tt) := id :: l
                                     | (local_const id _ _ _, tt) := id :: l
                                     | _ := l