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


            
            def Nat.foo : Nat → Nat

            
              | 0 => 0

            
              | n+1 => foo n

            
            decreasing_by decreasing_tactic


            theorem Nat.Bar.foo : foo 2 = 0 := by

            
              simp? [Nat.foo]
	def Nat.foo : Nat → Nat
	\| 0 => 0
	\| n+1 => foo n
	decreasing_by decreasing_tactic

	theorem Nat.Bar.foo : foo 2 = 0 := by
	simp? [Nat.foo]