mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
40e8f4c5fb
This PR turns on the new `do` elaborator in Init, Lean, Std, Lake and the testsuite. --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
8 lines
470 B
Plaintext
8 lines
470 B
Plaintext
bhaviksSampler.lean:98:4-98:11: warning: declaration uses `sorry`
|
|
bhaviksSampler.lean:98:4-98:11: warning: declaration uses `sorry`
|
|
bhaviksSampler.lean:117:4-117:8: warning: declaration uses `sorry`
|
|
bhaviksSampler.lean:117:4-117:8: warning: declaration uses `sorry`
|
|
bhaviksSampler.lean:126:8-126:18: warning: declaration uses `sorry`
|
|
bhaviksSampler.lean:129:8-129:25: warning: declaration uses `sorry`
|
|
bhaviksSampler.lean:152:8-152:23: warning: declaration uses `sorry`
|