issue !4#554: set as a TermElab

Stream: triage

[Random Issue Bot]

Today I chose issue 554 for discussion!

set as a TermElab
Created by @Alex J Best (@alexjbest) on 2022-11-07
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #554 for discussion!

set as a TermElab
Created by @Alex J Best (@alexjbest) on 2022-11-07
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #554 for discussion!

set as a TermElab
Created by @Alex J Best (@alexjbest) on 2022-11-07
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kyle Miller]

Closed the issue as completed, since the let (eq := h) syntax from lean4#8914 adds the unfolding equality.

def a (t : Nat) (h : t < 7) : Nat :=
  if t = 0 then 0 else
  let (eq := h) b : Nat := t - 1
  (a b (by rw [h]; sorry)) + 1