redefining def

Stream: lean4

[Reid Barton]

Is it easy to override def/theorem to, for example, add a specific user attribute to all definitions/theorems?

[Arthur Paulino]

Do you mean something like

defs f (n : Nat) : Nat := n

That would be equivalent to

@[simp] def f (n : Nat) : nat := n

?

[Reid Barton]

I think ideally I would like def f (n : Nat) : Nat := n to mean @[simp] def f (n : Nat) : Nat := n, after some top-level command has been run or a scope opened or whatever.

[Arthur Paulino]

Hm, someone more competent than myself might be able to answer this, but I don't know how to do that without triggering an infinite macro loop of def ⋯ replacement by @[simp] def ⋯

[Gabriel Ebner]

You should be able to add a scoped macro, like:

namespace Topos
scoped macro_rules
| `(def ...) => `(@[topos] def)
end Topos

open Topos -- now all defs are rewritten to @[topos] def
def foo := 42

[Gabriel Ebner]

Arthur Paulino said:

Hm, someone more competent than myself might be able to answer this, but I don't know how to do that without triggering an infinite macro loop of def ⋯ replacement by @[simp] def ⋯

Essentially you just need to do if attrs contains simp then throwUnsupported.

[Gabriel Ebner]

You can look at this (now obsolete) hack for inspiration: https://github.com/leanprover-community/mathlib4/blob/70af8b92010bdae02ef1228093764a936ba5b244/Mathlib/Tactic/Ext.lean#L77-L90

[Arthur Paulino]

So throwUnsupported will interrupt the macro expansion instead of signaling an error message? I didn't know that

[Sebastian Ullrich]

@[attr] section might also be a sensible option, though more likely as a built-in

[Reid Barton]

Thanks! Is the ... in | `(def ...) => `(@[topos] def) supposed to mean "put the syntax of def here"? I get an error "expected identifier" there

[Tomas Skrivan]

Here is macro that prints out all attributes:

syntax declModifiers "theorem " declId bracketedBinder* (":" term)? ":=" term  : command

macro_rules
  | `($mods:declModifiers theorem $id $params:bracketedBinder* $[: $ty:term]? := $body) => do

    dbg_trace "Theorem attributes are:"
    for i in [0:mods[1][0][1].getNumArgs/2+1] do
      dbg_trace s!"{mods[1][0][1][2*i][1][0]}"

    `($mods:declModifiers def $id $params:bracketedBinder* $[: $ty:term]? := $body)

@[simp, export hoho, extern "adsf"] theorem nat_add_comm (a b : Nat) : a + b = b + a := sorry

It prints out:

Theorem attributes are:
"simp"
"export"
"extern"

However, I had to change theorem to def such that the macro does not expand infinitely.

[Tomas Skrivan]

Also I do not understand the declModifiers parser. I got the sequence mods[1][0][1][2*i][1][0] by trial and error.