044bfdb098
This PR deprecates `let_fun` syntax in favor of `have` and removes `letFun` support from WHNF and `simp`.
6 lines
170 B
Text
6 lines
170 B
Text
consumePPHint.lean:8:8-8:14: warning: declaration uses 'sorry'
|
|
case a
|
|
⊢ q
|
|
(have x := 0;
|
|
x + 1)
|
|
consumePPHint.lean:10:8-10:15: warning: declaration uses 'sorry'
|