The classes GetElem and GetElem? implement lookup notation,
specifically xs[i], xs[i]?, xs[i]!, and xs[i]'p.
Both classes are indexed by types coll, idx, and elem which are
the collection, the index, and the element types.
A single collection may support lookups with multiple index
types. The relation valid determines when the index is guaranteed to be
valid; lookups of valid indices are guaranteed not to fail.
For example, an instance for arrays looks like
GetElem (Array α) Nat α (fun xs i => i < xs.size). In other words, given an
array xs and a natural number i, xs[i] will return an α when valid xs i
holds, which is true when i is less than the size of the array. Array
additionally supports indexing with USize instead of Nat.
In either case, because the bounds are checked at compile time,
no runtime check is required.
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 the return
value elem and side condition valid required to ensure xs[i] yields
a valid value of type elem. The tactic get_elem_tactic is
invoked to prove validity automatically. The xs[i]'p notation uses the
proof p to satisfy the validity condition.
If the proof p is long, it is often easier to place the
proof in the context using have, because get_elem_tactic tries
assumption.
The proof side-condition valid xs i is automatically dispatched by the
get_elem_tactic tactic; this tactic can be extended by adding more clauses to
get_elem_tactic_extensible using macro_rules.
xs[i]? and xs[i]! do not impose a proof obligation; the former returns
an Option elem, with none signalling that the value isn't present, and
the latter returns elem but panics if the value isn't there, returning
default : elem based on the Inhabited elem instance.
These are provided by the GetElem? class, for which there is a default instance
generated from a GetElem class as long as valid xs i is always decidable.
Important instances include:
-
arr[i] : α where arr : Array α and i : Nat or i : USize: does array
indexing with no runtime 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.
Instance Constructor
Extends
Methods
getElem : (xs : coll) → (i : idx) → valid xs i → elem
Inherited from
-
GetElem coll idx elem valid
getElem? : coll → idx → Option elem
The syntax arr[i]? gets the i'th element of the collection arr,
if it is present (and wraps it in some), and otherwise returns none.
Conventions for notations in identifiers:
getElem! : [Inhabited elem] → coll → idx → elem
The syntax arr[i]! gets the i'th element of the collection arr,
if it is present, and otherwise panics at runtime and returns the default term
from Inhabited elem.
Conventions for notations in identifiers:
