diff --git a/lakefile.lean b/lakefile.lean
index 81cf615..005af1a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -27,6 +27,7 @@ script build do
   if ← runCmd "python" #["-m", "lean2md", "lean", "md"] then return 1
   if ← runCmd "python" #["-m", "lean2md", "lean/main", "md/main"] then return 1
   if ← runCmd "python" #["-m", "lean2md", "lean/extra", "md/extra"] then return 1
+  if ← runCmd "python" #["-m", "lean2md", "lean/extra/attrs", "md/extra/atrs"] then return 1
 
   return 0
 
@@ -36,5 +37,6 @@ script viper_build do
   if ← runCmd "viper" #["-m", "lean2md", "lean", "md"] then return 1
   if ← runCmd "viper" #["-m", "lean2md", "lean/main", "md/main"] then return 1
   if ← runCmd "viper" #["-m", "lean2md", "lean/extra", "md/extra"] then return 1
+  if ← runCmd "viper" #["-m", "lean2md", "lean/extra/attrs", "md/extra/attrs"] then return 1
 
   return 0
diff --git a/lean-toolchain b/lean-toolchain
index b6f166c..99f81a4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-07-16
+leanprover/lean4:nightly-2022-07-25
diff --git a/lean/extra/attributes.lean b/lean/extra/attributes.lean
index e69de29..fdad209 100644
--- a/lean/extra/attributes.lean
+++ b/lean/extra/attributes.lean
@@ -0,0 +1,130 @@
+import lean.extra.attrs.dummy
+import lean.extra.attrs.tag
+-- import lean.extra.attrs.parametric
+-- import lean.extra.attrs.simp
+
+/-
+# Attributes
+
+Attributes in Lean allows one to perform preprocessing on definitions.
+They are similar to Python's decorators and Rust's proc-macros.
+
+Unfortunately, it turns out that attributes must be defined in a separate module, so
+we will bounce between this file and the files in the `attrs/` folder which
+contain the implementations of the attributes. We'll see you at
+[`./attrs/tag.lean`](./attrs/tag.lean).
+
+## Tag attributes with `myTag`
+
+see that we've created a tagging infrastructure based on Lean's `TagAttribute`s, which exists
+explicitly to allow us to create 'simple' attributes that wish to keep track of
+definitions that have been tagged with a given attribute, and nothing more.
+
+-/
+@[myTag]
+def tag1 : Int := 1
+
+@[myTag]
+def tag2 : Int := 2
+
+@[myTag]
+def tag3 : Int := 3
+
+/-
+See that we can access all the declarations that have been tagged with @[myTag].
+This simplified mechanism exists to allow us to easily tag definitions of interest.
+-/
+
+-- decl: tag3 | find? OfNat.ofNat.{0} Int 3 (Int.instOfNatInt 3)
+-- decl: tag1 | find? OfNat.ofNat.{0} Int 1 (Int.instOfNatInt 1)
+-- decl: tag2 | find? OfNat.ofNat.{0} Int 2 (Int.instOfNatInt 2)
+
+
+/-
+## Parametric attributes with `myParam`
+
+A parametric attribute is like a tag attribute, while adding support for
+parameters in the attribute.
+
+We shall add an attribute called `myParam`, which recieves two parameters,
+a priority, denoted by a natural number, and an optional tag `important`.
+
+
+We'll see you at [`./attrs/parametric.lean`](./attrs/dummy.lean).
+
+-/
+
+
+
+@[myParam 10] def h1 (x : Nat) := 2*x + 1
+@[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`
+
+We'll see you at [`./attrs/dummy.lean`](./attrs/dummy.lean).
+
+
+We run the `dummy_attr <number>`, and we see that we get access to the
+attribute argument <number>, the name of the declaration (`foo`), the type
+of the declaration (`int`), and the value of the declaration, which
+is the raw syntax tree.
+-/
+
+@[dummy_attr 0]
+def foo : Int := 42
+-- number + 1: 1
+-- src: foo | stx: (Attr.dummy_attr "dummy_attr" (num "0")) | kind: global
+-- srcDecl:
+--   name: foo
+--   type: Int
+--   value?: (some (OfNat.ofNat.{0} Int 42 (Int.instOfNatInt 42)))
+
+
+/-
+Below is an example of a declaration that does not have any value.
+-/
+
+@[dummy_attr 52]
+class bar
+-- number + 1: 53
+-- src: bar | stx: (Attr.dummy_attr "dummy_attr" (num "52")) | kind: global
+-- srcDecl:
+--   name: bar
+--   type: Type
+--   value?: none
+
+
+/-
+## Modifying the `value` with the `around` attribute
+
+We're going to write an attribute that will modify a given definition
+
+
+## Implementing `sym`:
+Scoped environment extension maintains scoping information, so it keeps track of
+whether the tag is local or not.
+-/
+
+
diff --git a/lean/extra/attrs/dummy.lean b/lean/extra/attrs/dummy.lean
new file mode 100644
index 0000000..d9517d5
--- /dev/null
+++ b/lean/extra/attrs/dummy.lean
@@ -0,0 +1,28 @@
+import Lean
+open Lean
+
+namespace Attr
+syntax (name := dummy_attr) "dummy_attr" term : attr
+
+/-
+This uses a low level attribute registration function. We declare the attribute
+with `registerBuiltinAttribute`. The `name` field is the name of the attribute, which
+should match with the `syntax` above for parsing. The `descr` is the textual description
+of the attribute used for docstrings. The `add` function is run when the attribute is applied to a
+declaration of name `declName`. `stx` is the syntax of the attribute including arguments
+-/
+initialize registerBuiltinAttribute {
+    name := `dummy_attr
+    descr :="dummy_attr print information"
+    add := fun declName stx kind => do
+      let num : Nat := stx[1].toNat
+      dbg_trace "number + 1: {num + 1}"
+      dbg_trace "declName: {declName} | stx: {stx} | kind: {kind}"
+      let srcDecl ← getConstInfo declName
+      dbg_trace "srcDecl:"
+      dbg_trace "  name: {srcDecl.name}"
+      dbg_trace "  type: {srcDecl.type}"
+      dbg_trace "  value?: {srcDecl.value?}"
+      return ()
+  }
+
diff --git a/lean/extra/attrs/parameteric.lean b/lean/extra/attrs/parameteric.lean
new file mode 100644
index 0000000..063d592
--- /dev/null
+++ b/lean/extra/attrs/parameteric.lean
@@ -0,0 +1,31 @@
+import Lean
+open Lean
+
+-- The name of the syntax is important. The name is
+-- used to connect to the corresponding attribute.
+syntax (name := myParam) "myParam" num "important"? : attr
+
+/-
+
+This declarares the attribute `myParamAttr`, which is parametrized
+by a value of type `(Nat × Bool)`. The `getParam` function describes how to build
+a value of `(Nat × Bool)` given the raw syntax declared by `myParam` above.
+The `afterSet` function can be used as a finalizer to perform processing once we have
+a parsed value.
+-/
+initialize fooParamAttr : ParametricAttribute (Nat × Bool) ←
+  registerParametricAttribute {
+    name := `myParam  /-
+       The attribute name must match the `syntax` declaration name.
+    -/
+    descr := "parametric attribute containing a priority and flag"
+    getParam := fun _ stx =>
+      match stx with
+      | `(attr| myParam $prio:num) =>
+          return (prio.getNat, false)
+      | `(attr| myParam $prio:num important) =>
+          return (prio.getNat, true)
+      | _  => throwError "unexpected foo attribute"
+    afterSet := fun declName val => do
+      IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}"
+  }
diff --git a/lean/extra/attrs/simp.lean b/lean/extra/attrs/simp.lean
new file mode 100644
index 0000000..467146f
--- /dev/null
+++ b/lean/extra/attrs/simp.lean
@@ -0,0 +1,9 @@
+import Lean
+
+/--
+We declare a simplifcation attribute using the keyword
+`register_simp_attr`, 
+-/
+register_simp_attr fooSimp "my own foo simp attribute"
+
+
diff --git a/lean/extra/attrs/tag.lean b/lean/extra/attrs/tag.lean
new file mode 100644
index 0000000..de93638
--- /dev/null
+++ b/lean/extra/attrs/tag.lean
@@ -0,0 +1,25 @@
+import Lean
+
+open Lean Meta System Std Elab Command
+
+
+initialize myTagAttribute : TagAttribute ←
+  registerTagAttribute `myTag "We are testing this custom tag."
+
+
+def listAllTagged : MetaM Unit := do
+    let env <- getEnv
+    for declName in myTagAttribute.ext.getState env do
+      let mval := env.find? declName
+      let mstr := match mval with | .none => "<none>" | .some v => toString v.value!
+      dbg_trace "decl: {declName} | find? {mstr}"
+    -- let x : NameSet := myTagAttribute.ext.getState env
+
+
+elab "listAllTagged" : command => do
+  liftTermElabM (some `listAllTagged) (listAllTagged)
+  return ()
+   
+  
+
+
diff --git a/md/extra/attributes.md b/md/extra/attributes.md
index 8b13789..82d0927 100644
--- a/md/extra/attributes.md
+++ b/md/extra/attributes.md
@@ -1 +1,119 @@
+```lean
+import lean.extra.attrs.dummy
+import lean.extra.attrs.tag
+-- import lean.extra.attrs.parametric
+-- import lean.extra.attrs.simp
+```
 
+# Attributes
+
+Attributes in Lean allows one to perform preprocessing on definitions.
+They are similar to Python's decorators and Rust's proc-macros.
+
+Unfortunately, it turns out that attributes must be defined in a separate module, so
+we will bounce between this file and the files in the `attrs/` folder which
+contain the implementations of the attributes. We'll see you at
+[`./attrs/tag.lean`](./attrs/tag.lean).
+
+## Tag attributes with `myTag`
+
+see that we've created a tagging infrastructure based on Lean's `TagAttribute`s, which exists
+explicitly to allow us to create 'simple' attributes that wish to keep track of
+definitions that have been tagged with a given attribute, and nothing more.
+
+```lean
+@[myTag]
+def tag1 : Int := 1
+
+@[myTag]
+def tag2 : Int := 2
+
+@[myTag]
+def tag3 : Int := 3
+```
+
+See that we can access all the declarations that have been tagged with @[myTag].
+This simplified mechanism exists to allow us to easily tag definitions of interest.
+
+```lean
+-- decl: tag3 | find? OfNat.ofNat.{0} Int 3 (Int.instOfNatInt 3)
+-- decl: tag1 | find? OfNat.ofNat.{0} Int 1 (Int.instOfNatInt 1)
+-- decl: tag2 | find? OfNat.ofNat.{0} Int 2 (Int.instOfNatInt 2)
+```
+
+## Parametric attributes with `myParam`
+
+A parametric attribute is like a tag attribute, while adding support for
+parameters in the attribute.
+
+We shall add an attribute called `myParam`, which recieves two parameters,
+a priority, denoted by a natural number, and an optional tag `important`.
+
+
+We'll see you at [`./attrs/parametric.lean`](./attrs/dummy.lean).
+
+```lean
+@[myParam 10] def h1 (x : Nat) := 2*x + 1
+@[myParam 20 important] def h2 (x : Nat) := 2*x + 1
+```
+
+## Using `simpAttr`
+
+```lean
+@[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`
+
+We'll see you at [`./attrs/dummy.lean`](./attrs/dummy.lean).
+
+
+We run the `dummy_attr <number>`, and we see that we get access to the
+attribute argument <number>, the name of the declaration (`foo`), the type
+of the declaration (`int`), and the value of the declaration, which
+is the raw syntax tree.
+
+```lean
+@[dummy_attr 0]
+def foo : Int := 42
+-- number + 1: 1
+-- src: foo | stx: (Attr.dummy_attr "dummy_attr" (num "0")) | kind: global
+-- srcDecl:
+--   name: foo
+--   type: Int
+--   value?: (some (OfNat.ofNat.{0} Int 42 (Int.instOfNatInt 42)))
+```
+
+Below is an example of a declaration that does not have any value.
+
+```lean
+@[dummy_attr 52]
+class bar
+-- number + 1: 53
+-- src: bar | stx: (Attr.dummy_attr "dummy_attr" (num "52")) | kind: global
+-- srcDecl:
+--   name: bar
+--   type: Type
+--   value?: none
+```
+
+## Modifying the `value` with the `around` attribute
+
+We're going to write an attribute that will modify a given definition
+
+
+## Implementing `sym`:
+Scoped environment extension maintains scoping information, so it keeps track of
+whether the tag is local or not.
diff --git a/md/extra/attrs/dummy.md b/md/extra/attrs/dummy.md
new file mode 100644
index 0000000..e08a497
--- /dev/null
+++ b/md/extra/attrs/dummy.md
@@ -0,0 +1,30 @@
+```lean
+import Lean
+open Lean
+
+namespace Attr
+syntax (name := dummy_attr) "dummy_attr" term : attr
+```
+
+This uses a low level attribute registration function. We declare the attribute
+with `registerBuiltinAttribute`. The `name` field is the name of the attribute, which
+should match with the `syntax` above for parsing. The `descr` is the textual description
+of the attribute used for docstrings. The `add` function is run when the attribute is applied to a
+declaration of name `declName`. `stx` is the syntax of the attribute including arguments
+
+```lean
+initialize registerBuiltinAttribute {
+    name := `dummy_attr
+    descr :="dummy_attr print information"
+    add := fun declName stx kind => do
+      let num : Nat := stx[1].toNat
+      dbg_trace "number + 1: {num + 1}"
+      dbg_trace "declName: {declName} | stx: {stx} | kind: {kind}"
+      let srcDecl ← getConstInfo declName
+      dbg_trace "srcDecl:"
+      dbg_trace "  name: {srcDecl.name}"
+      dbg_trace "  type: {srcDecl.type}"
+      dbg_trace "  value?: {srcDecl.value?}"
+      return ()
+  }
+```
diff --git a/md/extra/attrs/parameteric.md b/md/extra/attrs/parameteric.md
new file mode 100644
index 0000000..11e9f24
--- /dev/null
+++ b/md/extra/attrs/parameteric.md
@@ -0,0 +1,33 @@
+```lean
+import Lean
+open Lean
+
+-- The name of the syntax is important. The name is
+-- used to connect to the corresponding attribute.
+syntax (name := myParam) "myParam" num "important"? : attr
+```
+
+This declarares the attribute `myParamAttr`, which is parametrized
+by a value of type `(Nat × Bool)`. The `getParam` function describes how to build
+a value of `(Nat × Bool)` given the raw syntax declared by `myParam` above.
+The `afterSet` function can be used as a finalizer to perform processing once we have
+a parsed value.
+
+initialize fooParamAttr : ParametricAttribute (Nat × Bool) ←
+  registerParametricAttribute {
+    name := `myParam  /-
+       The attribute name must match the `syntax` declaration name.
+
+```lean
+descr := "parametric attribute containing a priority and flag"
+    getParam := fun _ stx =>
+      match stx with
+      | `(attr| myParam $prio:num) =>
+          return (prio.getNat, false)
+      | `(attr| myParam $prio:num important) =>
+          return (prio.getNat, true)
+      | _  => throwError "unexpected foo attribute"
+    afterSet := fun declName val => do
+      IO.println s!"set attribute [myParam] at {declName}; priority: {val.1}; important? {val.2}"
+  }
+```
diff --git a/md/extra/attrs/simp.md b/md/extra/attrs/simp.md
new file mode 100644
index 0000000..ad579e3
--- /dev/null
+++ b/md/extra/attrs/simp.md
@@ -0,0 +1,11 @@
+```lean
+import Lean
+```
+
+-
+We declare a simplifcation attribute using the keyword
+`register_simp_attr`,
+
+```lean
+register_simp_attr fooSimp "my own foo simp attribute"
+```
diff --git a/md/extra/attrs/tag.md b/md/extra/attrs/tag.md
new file mode 100644
index 0000000..09a863b
--- /dev/null
+++ b/md/extra/attrs/tag.md
@@ -0,0 +1,23 @@
+```lean
+import Lean
+
+open Lean Meta System Std Elab Command
+
+
+initialize myTagAttribute : TagAttribute ←
+  registerTagAttribute `myTag "We are testing this custom tag."
+
+
+def listAllTagged : MetaM Unit := do
+    let env <- getEnv
+    for declName in myTagAttribute.ext.getState env do
+      let mval := env.find? declName
+      let mstr := match mval with | .none => "<none>" | .some v => toString v.value!
+      dbg_trace "decl: {declName} | find? {mstr}"
+    -- let x : NameSet := myTagAttribute.ext.getState env
+
+
+elab "listAllTagged" : command => do
+  liftTermElabM (some `listAllTagged) (listAllTagged)
+  return ()
+```