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


            
            def u (x : Nat) : Nat := do

            
              let y := x + x

            
              y * (if y > 100 then 1 else (5 : Nat))
	def u (x : Nat) : Nat := do
	let y := x + x
	y * (if y > 100 then 1 else (5 : Nat))