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


            
            def sum (as : Array Nat) : Nat :=

            
              let rec go (i : Nat) (s : Nat) : Nat :=

            
                if h : i < as.size then

            
                  go (i+2) (s + as.get ⟨i, h⟩) -- Error

            
                else

            
                  s

            
                termination_by as.size - i

            
              go 0 0
	def sum (as : Array Nat) : Nat :=
	let rec go (i : Nat) (s : Nat) : Nat :=
	if h : i < as.size then
	go (i+2) (s + as.get ⟨i, h⟩) -- Error
	else
	s
	termination_by as.size - i
	go 0 0