adding a new declaration

Stream: metaprogramming / tactics

[Arthur Paulino]

Suppose I'm in CommandElabM and I have

...
let arr : ByteArray := .mk #[42]
let nam : Name := `foo

What's the best way to add foo to my environment bound to arr these days? (I'm on 4.16)

As if I were doing def foo : ByteArray := .mk #[42]

[Arthur Paulino]

Oh wow, ChatGPT actually got it :explode:

  let decl := Declaration.defnDecl {
    name        := `foo
    levelParams := []
    type        := mkConst ``ByteArray
    value       := mkApp (mkConst ``ByteArray.mk) (toExpr arr.data)
    hints       := ReducibilityHints.opaque
    safety      := DefinitionSafety.safe
  }
  liftCoreM $ addAndCompile decl

I had to nudge it because ByteArray doesn't implement ToExpr and also because addAndCompile needs CoreM lifting beforehand. But then it was able to correct itself. It's pretty hype that Lean 4 has been absorbed by ChatGPT :tada:

[Adam Topaz]

Here's another option:

import Lean

open Lean

-- HACK!
instance : Quote UInt8 where
  quote n := Syntax.mkNatLit n.toNat

#eval show Elab.Command.CommandElabM Unit from do
  let arr : ByteArray := .mk #[42]
  let arrStx : TSyntax `term := quote arr.data
  let nam : Name := `foo
  let stx ← `(command| def $(mkIdent nam) := ByteArray.mk $arrStx)
  Elab.Command.elabCommand stx

#eval foo