Lean4
/-- A helper function for constructing a related declaration from an existing one.
This is currently used by the attributes `reassoc` and `elementwise`,
and has been factored out to avoid code duplication.
Feel free to add features as needed for other applications.
This helper:
* calls `addDeclarationRangesFromSyntax`, so jump-to-definition works,
* copies the `protected` status of the existing declaration, and
* supports copying attributes.
Arguments:
* `src : Name` is the existing declaration that we are modifying.
* `suffix : String` will be appended to `src` to form the name of the new declaration.
* `ref : Syntax` is the syntax where the user requested the related declaration.
* `construct type value levels : MetaM (Expr × List Name)`
given the type, value, and universe variables of the original declaration,
should construct the value of the new declaration,
along with the names of its universe variables.
* `attrs` is the attributes that should be applied to both the new and the original declaration,
e.g. in the usage `@[reassoc (attr := simp)]`.
We apply it to both declarations, to have the same behavior as `to_additive`, and to shorten some
attribute commands. Note that `@[elementwise (attr := simp), reassoc (attr := simp)]` will try
to apply `simp` twice to the current declaration, but that causes no issues.
-/
def addRelatedDecl (src : Name) (suffix : String) (ref : Syntax)
(attrs? : Option (Syntax.TSepArray `Lean.Parser.Term.attrInstance ","))
(construct : Expr → Expr → List Name → MetaM (Expr × List Name)) : MetaM Unit := do
let tgt :=
match src with
| Name.str n s => Name.mkStr n <| s ++ suffix
| x => x
addDeclarationRangesFromSyntax tgt (← getRef) ref
let info ← getConstInfo src
let (newValue, newLevels) ← construct info.type info.value! info.levelParams
let newValue ← instantiateMVars newValue
let newType ← instantiateMVars (← inferType newValue)
match info with
| ConstantInfo.thmInfo info =>
addAndCompile <| .thmDecl { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
| ConstantInfo.defnInfo info =>
-- Structure fields are created using `def`, even when they are propositional,
-- so we don't rely on this to decide whether we should be constructing a `theorem` or a `def`.
addAndCompile <|
if ← isProp newType then
.thmDecl { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
else .defnDecl { info with levelParams := newLevels, type := newType, name := tgt, value := newValue }
| _ =>
throwError "Constant {src} is not a theorem or definition."
if isProtected (← getEnv) src then
setEnv <| addProtected (← getEnv) tgt
inferDefEqAttr tgt
let attrs :=
match attrs? with
| some attrs => attrs
| none => #[]
_ ←
Term.TermElabM.run' <| do
let attrs ← elabAttrs attrs
Term.applyAttributes src attrs
Term.applyAttributes tgt attrs
