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


            
            def g (x : Nat) (y : Nat) : Nat :=

            
              if x < y then

            
                2 * g (x-1) y -- Error here

            
              else

            
                0

            
            termination_by x
	def g (x : Nat) (y : Nat) : Nat :=
	if x < y then
	2 * g (x-1) y -- Error here
	else
	0
	termination_by x