max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/doNotation6.lean.out.expected
Sebastian Graf 40e8f4c5fb
chore: turn on new do elaborator in Core (#12656) 
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>
2026-03-09 12:38:33 +00:00

1 line
143 B
Text
Raw Permalink Blame History

doNotation6.lean:22:0-22:6: warning: This `do` element and its control-flow region are dead code. Consider refactoring your code to remove it.
Reference in a new issue View git blame Copy permalink