Core.Index — oppi

PréludeChargé par défaut — aucun import nécessaire.

Accès par indice et mise à jour indexée

Synopsis

panic : String -> a
listAt : List a -> Nat -> Maybe a
listSetAt : List a -> Nat -> a -> List a
goListSet : List a -> List a -> Nat -> a -> List a
(!) : List a -> Nat -> Maybe a
index : List a -> Nat -> a
set : List a -> Nat -> a -> List a

panic : String -> a

Interrompt le programme avec un message — une erreur irrécupérable (contrairement à l'effet Throw rattrapable). Sous-tend c[i] / index quand l'indice est hors bornes.

listAt : List a -> Nat -> Maybe a

listSetAt : List a -> Nat -> a -> List a

goListSet : List a -> List a -> Nat -> a -> List a

(!) : List a -> Nat -> Maybe a

Indice sûr xs[i]? — Nothing si i est hors bornes.

index : List a -> Nat -> a

Indice direct xs[i] — panique si i est hors bornes.

set : List a -> Nat -> a -> List a

set xs i v — une nouvelle liste avec la position i mise à v (inchangée si i est hors bornes). La notation xs { [i] := v } est équivalente (gardée — décision Q3 du 2026-07-02 — mais set est la forme à enseigner et à documenter).