class GetElem (coll : Type u) (idx : Type v) (elem : outParam (Type w)) (valid : outParam (coll → idx → Prop)) : Type (max (max u v) w)

The class GetElem coll idx elem valid implements the xs[i] notation. Given xs[i] with xs : coll and i : idx, Lean looks for an instance of GetElem coll idx elem valid and uses this to infer the type of return value elem and side conditions valid required to ensure xs[i] yields a valid value of type elem.

For example, the instance for arrays looks like GetElem (Array α) Nat α (fun xs i => i < xs.size).

The proof side-condition valid xs i is automatically dispatched by the get_elem_tactic tactic, which can be extended by adding more clauses to get_elem_tactic_trivial.

• getElem : (xs : coll) → (i : idx) → valid xs i → elem

  The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

  The actual behavior of this class is type-dependent, but here are some important implementations:

  • arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no bounds check and a proof side goal i < arr.size.
  • l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
  • stx[i] : Syntax where stx : Syntax and i : Nat: get a syntax argument, no side goal (returns .missing out of range)

  There are other variations on this syntax:

  • arr[i]! is syntax for getElem! arr i which should panic and return default : α if the index is not valid.
  • arr[i]? is syntax for getElem? which should return none if the index is not valid.
  • arr[i]'h is syntax for getElem arr i h with h an explicit proof the index is valid.
• getElem? : (xs : coll) → (i : idx) → [inst : Decidable (valid xs i)] → Option elem
• getElem! : [inst : Inhabited elem] → (xs : coll) → (i : idx) → [inst : Decidable (valid xs i)] → elem

def «term__[_]» : Lean.TrailingParserDescr

The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

The actual behavior of this class is type-dependent, but here are some important implementations:

• arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no bounds check and a proof side goal i < arr.size.
• l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
• stx[i] : Syntax where stx : Syntax and i : Nat: get a syntax argument, no side goal (returns .missing out of range)

There are other variations on this syntax:

• arr[i]! is syntax for getElem! arr i which should panic and return default : α if the index is not valid.
• arr[i]? is syntax for getElem? which should return none if the index is not valid.
• arr[i]'h is syntax for getElem arr i h with h an explicit proof the index is valid.

Equations

• One or more equations did not get rendered due to their size.

def «term__[_]'_» : Lean.TrailingParserDescr

The syntax arr[i] gets the i'th element of the collection arr. If there are proof side conditions to the application, they will be automatically inferred by the get_elem_tactic tactic.

The actual behavior of this class is type-dependent, but here are some important implementations:

• arr[i] : α where arr : Array α and i : Nat or i : USize: does array indexing with no bounds check and a proof side goal i < arr.size.
• l[i] : α where l : List α and i : Nat: index into a list, with proof side goal i < l.length.
• stx[i] : Syntax where stx : Syntax and i : Nat: get a syntax argument, no side goal (returns .missing out of range)

There are other variations on this syntax:

• arr[i]! is syntax for getElem! arr i which should panic and return default : α if the index is not valid.
• arr[i]? is syntax for getElem? which should return none if the index is not valid.
• arr[i]'h is syntax for getElem arr i h with h an explicit proof the index is valid.

Equations

• One or more equations did not get rendered due to their size.

def «term__[_]_?» : Lean.TrailingParserDescr

The syntax arr[i]? gets the i'th element of the collection arr or returns none if i is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

def «term__[_]_!» : Lean.TrailingParserDescr

The syntax arr[i]! gets the i'th element of the collection arr and panics i is out of bounds.

Equations

• One or more equations did not get rendered due to their size.

class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w)) (dom : outParam (cont → idx → Prop)) [ge : GetElem cont idx elem dom] : Prop

• getElem?_def : ∀ (c : cont) (i : idx) [inst : Decidable (dom c i)], c[i]? = if h : dom c i then some c[i] else none
• getElem!_def : ∀ [inst : Inhabited elem] (c : cont) (i : idx) [inst_1 : Decidable (dom c i)], c[i]! = match c[i]? with | some e => e | none => default

theorem LawfulGetElem.getElem?_def {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)} [ge : GetElem cont idx elem dom] [self : LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]? = if h : dom c i then some c[i] else none

theorem LawfulGetElem.getElem!_def {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)} [ge : GetElem cont idx elem dom] [self : LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) [Decidable (dom c i)] : c[i]! = match c[i]? with | some e => e | none => default

theorem getElem?_pos {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]? = some c[i]

theorem getElem?_neg {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]? = none

theorem getElem!_pos {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] : c[i]! = c[i]

theorem getElem!_neg {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [GetElem cont idx elem dom] [LawfulGetElem cont idx elem dom] [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default

instance Fin.instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs ↑i

Equations

• One or more equations did not get rendered due to their size.

instance Fin.instLawfulGetElemValOfNat {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] : LawfulGetElem cont (Fin n) elem fun (xs : cont) (i : Fin n) => dom xs ↑i

Equations

• ⋯ = ⋯

@[simp]

theorem Fin.getElem_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a ↑i) : a[i] = a[↑i]

@[simp]

theorem Fin.getElem?_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {n : Nat} [h : GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a ↑i)] : a[i]? = a[↑i]?

@[simp]

theorem Fin.getElem!_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a ↑i)] [Inhabited Elem] : a[i]! = a[↑i]!

instance List.instGetElemNatLtLength {α : Type u_1} : GetElem (List α) Nat α fun (as : List α) (i : Nat) => i < as.length

Equations

• One or more equations did not get rendered due to their size.

instance List.instLawfulGetElemNatLtLength {α : Type u_1} : LawfulGetElem (List α) Nat α fun (as : List α) (i : Nat) => i < as.length

Equations

• ⋯ = ⋯

@[simp]

theorem List.cons_getElem_zero {α : Type u_1} (a : α) (as : List α) (h : 0 < (a :: as).length) : (a :: as)[0] = a

@[simp]

theorem List.cons_getElem_succ {α : Type u_1} (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : (a :: as)[i + 1] = as[i]

theorem List.get_drop_eq_drop {α : Type u_1} (as : List α) (i : Nat) (h : i < as.length) : as[i] :: List.drop (i + 1) as = List.drop i as

instance Array.instGetElemNatLtSize {α : Type u_1} : GetElem (Array α) Nat α fun (xs : Array α) (i : Nat) => i < xs.size

Equations

• One or more equations did not get rendered due to their size.

instance Array.instLawfulGetElemNatLtSize {α : Type u_1} : LawfulGetElem (Array α) Nat α fun (xs : Array α) (i : Nat) => i < xs.size

Equations

• ⋯ = ⋯

instance Lean.Syntax.instGetElemNatTrue : GetElem Lean.Syntax Nat Lean.Syntax fun (x : Lean.Syntax) (x : Nat) => True

Equations

• One or more equations did not get rendered due to their size.

instance Lean.Syntax.instLawfulGetElemNatTrue : LawfulGetElem Lean.Syntax Nat Lean.Syntax fun (x : Lean.Syntax) (x : Nat) => True

Equations

• Lean.Syntax.instLawfulGetElemNatTrue = ⋯