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


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

            
              if x < y then

            
                2 * id (g (x-1)) y

            
              else

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