poke

Author: hargoniX

src/Init/GetElem.lean

@@ -410,6 +410,7 @@ instance : LawfulGetElem (Array α) Nat α fun xs i => i < xs.size where
     a.get!Internal i = a[i]! := by
   simp only [get!Internal, getD, getInternal_eq_getElem, getElem!_def]
   split <;> simp_all [getElem?_pos, getElem?_neg]
+  simp [default]
 
 end Array
 

src/Init/Prelude.lean

@@ -3252,16 +3252,16 @@ Version of `Array.get!Internal` that does not increment the reference count of i
 This is only intended for direct use by the compiler.
 -/
 @[extern "lean_array_get_borrowed"]
-unsafe opaque Array.get!InternalBorrowed {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α
+unsafe opaque Array.get!InternalBorrowed {α : Type u} [inst : Inhabited (Unit → α)] (a : @& Array α) (i : @& Nat) : α := inst.default ()
 
 /--
 Use the indexing notation `a[i]!` instead.
 
 Access an element from an array, or panic if the index is out of bounds.
 -/
 @[extern "lean_array_get"]
-def Array.get!Internal {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
-  Array.getD a i default
+def Array.get!Internal {α : Type u} [inst : Inhabited (Unit → α)] (a : @& Array α) (i : @& Nat) : α :=
+  Array.getD a i (inst.default ())
 
 /--
 Adds an element to the end of an array. The resulting array's size is one greater than the input

src/Lean/Compiler/LCNF/ExtractClosed.lean

@@ -127,7 +127,6 @@ partial def visitCode (code : Code) : M Code := do
   match code with
   | .let decl k =>
     let should ← shouldExtractLetValue true decl.value
-    trace[Meta.debug] m!"Should extract: {← ppLetValue decl.value}? {should}"
     if should then
       let ⟨_, decls⟩ ← extractLetValue decl.value |>.run {}
       let decls := decls.reverse.push (.let decl)

src/include/lean/lean.h

@@ -844,7 +844,7 @@ static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
-    return lean_array_get_panic(def_val);
+    return lean_array_get_panic(lean_apply_1(def_val, lean_box(0)));
 }
 
 static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
@@ -859,7 +859,7 @@ static inline lean_object * lean_array_get_borrowed(lean_obj_arg def_val, b_lean
        i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
        but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
        In both cases, we would be out-of-memory. */
-    return lean_array_get_panic(def_val);
+    return lean_array_get_panic(lean_apply_1(def_val, lean_box(0)));
 }
 
 LEAN_EXPORT lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);