tests/compiler/StackOverflow.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            partial def foo : Nat → Nat | n => foo n + 1

            
            @[never_extract]

            
            def main : IO Unit := IO.println $ foo 0
	partial def foo : Nat → Nat \| n => foo n + 1
	@[never_extract]
	def main : IO Unit := IO.println $ foo 0