Skip to content

Commit

Permalink
feat: unify equational theorems between wf and structural recursion
Browse files Browse the repository at this point in the history
by removing the `tryRefl` variation between the two.

Part of #3983
  • Loading branch information
nomeata committed Aug 15, 2024
1 parent 8c96d21 commit bcf5fd8
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 7 deletions.
6 changes: 1 addition & 5 deletions src/Lean/Elab/PreDefinition/Eqns.lean
Original file line number Diff line number Diff line change
Expand Up @@ -228,16 +228,12 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
throwThe Unit ()
return (← (find e).run) matches .error _

partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]
return eqnTypes
where
go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
if tryRefl then
if (← tryURefl mvarId) then
saveEqn mvarId
return ()

if let some mvarId ← expandRHS? mvarId then
return (← go mvarId)
Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Elab/PreDefinition/Structural/Eqns.lean
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
let us := info.levelParams.map mkLevelParam
let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
let goal ← mkFreshExprSyntheticOpaqueMVar target
mkEqnTypes (tryRefl := true) info.declNames goal.mvarId!
mkEqnTypes info.declNames goal.mvarId!
let baseName := info.declName
let mut thmNames := #[]
for i in [: eqnTypes.size] do
Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Elab/PreDefinition/WF/Eqns.lean
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
let goal ← mkFreshExprSyntheticOpaqueMVar target
withReducible do
mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
mkEqnTypes info.declNames goal.mvarId!
let mut thmNames := #[]
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
Expand Down

0 comments on commit bcf5fd8

Please sign in to comment.