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


            
            def step : Array Nat := Array.mk (List.range 10)

            
            def main : IO Unit := IO.print s!"{step.size}\n"
	def step : Array Nat := Array.mk (List.range 10)
	def main : IO Unit := IO.print s!"{step.size}\n"