is there an equivalent way to auto generate function defs?

Stream: new members

[Alok Singh]

this is from some julia code in https://github.com/chakravala/Grassmann.jl/commit/280111c8d5826b6b8010b58e1ce0ea8329e67b86

for op ∈ (:acoth,:acot,:sinc,:cosc)
    @eval @inline Base.$op(::Infinity{V}) where V = Zero(V)
end

Does lean have a way to generate whats basically def acoth infinity := 0, besides writing them out?

[Eric Wieser]

Sure:

import Lean

run_cmd do
  for name in [`hello, `world] do
    Lean.Elab.Command.elabCommandTopLevel <|
      ← `(def $(Lean.mkIdent name) : Nat := 1)

#check hello
#check world