2 files changed, 2 insertions(+), 2 deletions(-)

M Demo/Imperative.lean
M Demo/Vec.lean

@@ 1,4 1,4 @@
-def List.countNumElements {a} (l : List a) : Nat := do
+def List.countNumElements {a} (l : List a) : Id Nat := do
   let mut num := 20
   for element in l do
     num := num + 1

@@ 8,7 8,7 @@ namespace Vec
   def cons {n} (v : Vec n α) (a : α) : Vec (Nat.succ n) α :=
       ⟨Array.mk $ a::v.as.data, by
         have (Array.mk $ a::v.as.data).size = (a::v.as.data).length by rfl
-        rw [this, List.lengthConsEq]
+        rw [this, List.length_cons]
         have v.as.data.length = n from v.pf
         rw this⟩