add simp attribute

Author: bollu

lean/extra/attributes.lean

@@ -1,6 +1,7 @@
 import lean.extra.attrs.dummy
 import lean.extra.attrs.tag
 import lean.extra.attrs.parametric
+import lean.extra.attrs.simp
 /-
 # Attributes
 
@@ -58,6 +59,26 @@ We'll see you at [`./attrs/parametric.lean`](./attrs/dummy.lean).
 @[myParam 20 important] def h2 (x : Nat) := 2*x + 1
 
 
+/-
+## Using `simpAttr`
+-/
+
+@[my_simp] theorem f_eq : f x = x + 2 := rfl
+@[my_simp] theorem g_eq : g x = x + 1 := rfl
+
+example : f x + g x = 2*x + 3 := by
+  simp_arith -- does not appy f_eq and g_eq
+  simp_arith [f, g]
+
+example : f x + g x = 2*x + 3 := by
+  simp_arith [my_simp]
+
+example : f x = id (x + 2) := by
+  simp
+  simp [my_simp]
+
+
+
 /-
 ## Using `dummy_attr`
 

lean/extra/attrs/around.lean

@@ -34,8 +34,17 @@ initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameM
     name          := `renameMapExtension
     addEntryFn    := RenameMap.insertPair
     addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es
+    initial       := sorry
   }
 
+/- 
+The key is Name × Name, and the value is RenameMap.
+The entires are written into the `olean` files.
+The functions `addEntryFn` tells us how to compute the values from the keys.
+So the values are "just" a caching mechanism for the keys, where the keys tell us
+what data is to be stored.
+-/
+
 def findRename? (env : Environment) : Name → Option Name :=
   (renameExtension.getState env).find?
 

lean/extra/attrs/simp.lean

@@ -0,0 +1,3 @@
+register_simp_attr fooSimp "my own foo simp attribute"
+
+