Nuprl Definition : array
array{i:l}(Val;n) ==
Arr:Type
× idx:ℕn ⟶ Arr ⟶ Val
× upd:ℕn ⟶ Val ⟶ Arr ⟶ Arr
× newarray:Val ⟶ Arr
× ∀[i:ℕn]. ∀[v:Val]. ((idx i (newarray v)) = v ∈ Val)
× (∀[i,j:ℕn]. ∀[x:Arr]. ∀[v:Val]. ((idx i (upd j v x)) = if (i =z j) then v else idx i x fi ∈ Val))
Definitions occuring in Statement :
int_seg: {i..j-},
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
uall: ∀[x:A]. B[x],
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
universe: Type,
function: x:A ⟶ B[x],
product: x:A × B[x],
int_seg: {i..j-},
natural_number: $n,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a
FDL editor aliases :
array
Latex:
array\{i:l\}(Val;n) ==
Arr:Type
\mtimes{} idx:\mBbbN{}n {}\mrightarrow{} Arr {}\mrightarrow{} Val
\mtimes{} upd:\mBbbN{}n {}\mrightarrow{} Val {}\mrightarrow{} Arr {}\mrightarrow{} Arr
\mtimes{} newarray:Val {}\mrightarrow{} Arr
\mtimes{} \mforall{}[i:\mBbbN{}n]. \mforall{}[v:Val]. ((idx i (newarray v)) = v)
\mtimes{} (\mforall{}[i,j:\mBbbN{}n]. \mforall{}[x:Arr]. \mforall{}[v:Val]. ((idx i (upd j v x)) = if (i =\msubz{} j) then v else idx i x fi ))
Date html generated:
2016_05_15-PM-02_17_12
Last ObjectModification:
2015_09_23-AM-07_38_24
Theory : monads
Home
Index