Update Lean to current nightly

Author: ineol

ELFSage/Types/ELFHeader.lean

@@ -72,7 +72,7 @@ def ELFHeader.ph_end [ELFHeader α] (eh : α) :=
 
 instance [ELFHeader α] : ToString α where
   toString eh :=
-    let ident (i : Fin 16) := (ELFHeader.e_ident eh).bytes.get ⟨ i, by simp [(ELFHeader.e_ident eh).sized] ⟩
+    let ident (i : Fin 16) := (ELFHeader.e_ident eh).bytes[i]'(by simp [(ELFHeader.e_ident eh).sized])
     let identAsHex (i: Fin 16) := toHex (ident i).toNat
     let identAsHexLength2 (i: Fin 16) := toHexMinLength (ident i).toNat 2
     "ElfHeader {\n" ++
@@ -149,7 +149,7 @@ def mkELF64Header (bs : ByteArray) (h : bs.size ≥ 0x40) : ELF64Header := {
   e_shnum     := getUInt16from 0x3C (by omega),
   e_shstrndx  := getUInt16from 0x3E (by omega),
 } where
-  isBigEndian := bs.get ⟨0x5,by omega⟩ == 2
+  isBigEndian := bs[0x5] == 2
   getUInt16from := if isBigEndian then bs.getUInt16BEfrom else bs.getUInt16LEfrom
   getUInt32from := if isBigEndian then bs.getUInt32BEfrom else bs.getUInt32LEfrom
   getUInt64from := if isBigEndian then bs.getUInt64BEfrom else bs.getUInt64LEfrom
@@ -243,7 +243,7 @@ def mkELF32Header (bs : ByteArray) (h : bs.size ≥ 0x34) : ELF32Header := {
   e_shnum     := getUInt16from 0x30 (by omega),
   e_shstrndx  := getUInt16from 0x32 (by omega),
 } where
-  isBigEndian := bs.get ⟨0x5,by omega⟩ == 2
+  isBigEndian := bs[0x5] == 2
   getUInt16from := if isBigEndian then bs.getUInt16BEfrom else bs.getUInt16LEfrom
   getUInt32from := if isBigEndian then bs.getUInt32BEfrom else bs.getUInt32LEfrom
 
@@ -311,7 +311,7 @@ instance : ELFHeader RawELFHeader where
 
 def mkRawELFHeader? (bs : ByteArray) : Except String RawELFHeader :=
   if h : bs.size < 5 then throw "Can't determine if this is a 32 or 64 bit binary (not enough bytes)."
-  else match bs.get ⟨0x4, by omega⟩ with
+  else match bs[0x4] with
   | 1 => .elf32 <$> mkELF32Header? bs
   | 2 => .elf64 <$> mkELF64Header? bs
   | _ => throw "Can't determine if this is a 32 of 64 bit binary (byte 0x5 of the elf header is bad)"

ELFSage/Types/File.lean

@@ -125,7 +125,7 @@ inductive RawELFFile where
 
 def mkRawELFFile? (bytes : ByteArray) : Except String RawELFFile :=
   if h : bytes.size < 5 then throw "Can't determine if this is a 32 or 64 bit binary (not enough bytes)."
-  else match bytes.get ⟨0x4, by omega⟩ with
+  else match bytes[0x4] with
   | 1 => .elf32 <$> mkELF32File? bytes
   | 2 => .elf64 <$> mkELF64File? bytes
   | _ => throw "Can't determine if this is a 32 of 64 bit binary (byte 0x5 of the elf header is bad)"

ELFSage/Types/SymbolTable.lean

@@ -45,8 +45,8 @@ def mkELF64SymbolTableEntry
   (h : bs.size - offset ≥ 0x18) :
   ELF64SymbolTableEntry := {
     st_name  := getUInt32from (offset + 0x00) (by omega),
-    st_info  := bs.get ⟨offset + 0x4, by omega⟩,
-    st_other := bs.get ⟨offset + 0x5, by omega⟩,
+    st_info  := bs[offset + 0x4]
+    st_other := bs[offset + 0x5]
     st_shndx := getUInt16from (offset + 0x6) (by omega),
     st_value := getUInt64from (offset + 0x8) (by omega),
     st_size  := getUInt64from (offset + 0x10) (by omega),
@@ -87,8 +87,8 @@ def mkELF32SymbolTableEntry
     st_name  := getUInt32from (offset + 0x00) (by omega),
     st_value := getUInt32from (offset + 0x04) (by omega),
     st_size  := getUInt32from (offset + 0x08) (by omega),
-    st_info  := bs.get ⟨offset + 0x9, by omega⟩,
-    st_other := bs.get ⟨offset + 0xa, by omega⟩,
+    st_info  := bs[offset + 0x9],
+    st_other := bs[offset + 0xa],
     st_shndx := getUInt16from (offset + 0xb) (by omega) ,
   } where
     getUInt16from := if isBigEndian then bs.getUInt16BEfrom else bs.getUInt16LEfrom