tests/elab/wfOmega.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            /-! A wf recursive definition that needs omega to work -/


            def foo (n : Nat) :=

            
              if h : n < 99 then 0 else foo (n - 99)
	/-! A wf recursive definition that needs omega to work -/

	def foo (n : Nat) :=
	if h : n < 99 then 0 else foo (n - 99)