Proposal
This seems to be a useful pattern:
for h : i in [:hs.size] do
let h := hs[i]'h.2
and it it is used in a few places (ok, quite a few written by me):
~/build/lean $ grep -F "]'h.2" **/*.lean
aesop/Aesop/BuiltinRules/Subst.lean: let (.fvar fvarId) := fvarSubst.get $ fvarIds[i]'h.2 | throwError
aesop/Aesop/Script.lean: let step := script[i]'h.2
lean4/src/Lean/Elab/PreDefinition/WF/Fix.lean: a' := a'.push (a[i]'h.2)
lean4/src/Lean/Elab/PreDefinition/WF/GuessLex.lean: let n ← (xs[i]'h.2).fvarId!.getUserName
lean4/src/Lean/Elab/PreDefinition/WF/GuessLex.lean: let measure := measures[measureIdx]'h.2
lean4/src/Lean/Elab/PreDefinition/WF/GuessLex.lean: let vars := (varNamess[funIdx]'h.2).map mkIdent
mathlib4/Mathlib/Tactic/Linarith/Frontend.lean: let (k', vs) := self[i]'h.2
mathlib4/Mathlib/Tactic/Linarith/Frontend.lean: if ← isDefEq (self[i]'h.2).1 k then
std4/Std/Lean/Meta/AssertHypotheses.lean: let h := hs[i]'h.2
std4/Std/Tactic/TryThis.lean: let .ok newText := (suggestions[i]'h.2).getObjValAs? String "suggestion" | panic! "bad type"
It would be nice if this worked out of the box. Here is one way of implementing that:
macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| exact Membership.mem.upper (by assumption))
Live action
Community Feedback
Zulip discussions:
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
Proposal
This seems to be a useful pattern:
and it it is used in a few places (ok, quite a few written by me):
It would be nice if this worked out of the box. Here is one way of implementing that:
Live action
Community Feedback
Zulip discussions:
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.