Nuprl Definition : map-sig
map-sig{i:l}(Key;Value) ==
"map":{m:Type| (valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))}
"eqKey":EqDecider(Key)
"find":Key ─→ self."map" ─→ (Value?)
"inDom":{f:Key ─→ self."map" ─→ 𝔹| ∀k:Key. ∀m:self."map". (↑(f k m) ⇐⇒ ↑isl(self."find" k m))}
"empty":{m:self."map"| ∀k:Key. (¬↑(self."inDom" k m))}
"isEmpty":{f:self."map" ─→ 𝔹| ∀m:self."map". (↑(f m) ⇐⇒ ∀k:Key. (¬↑(self."inDom" k m)))}
"update":{f:Key ─→ Value ─→ self."map" ─→ self."map"|
∀m:self."map". ∀k1,k2:Key. ∀v:Value.
((self."find" k1 (f k2 v m)) = if self."eqKey" k1 k2 then inl v else self."find" k1 m fi ∈ (Value?))}
"add":{f:Key ─→ Value ─→ self."map" ─→ self."map"|
∀m:self."map". ∀k1,k2:Key. ∀v:Value.
((self."find" k1 (f k2 v m))
= if (self."eqKey" k1 k2) ∧b (¬b(self."inDom" k2 m)) then inl v else self."find" k1 m fi
∈ (Value?))}
"remove":{f:Key ─→ self."map" ─→ self."map"|
∀m:self."map". ∀k1,k2:Key.
((self."find" k1 (f k2 m)) = if self."eqKey" k1 k2 then inr ⋅ else self."find" k1 m fi ∈ (Value?))}
Definitions occuring in Statement :
deq: EqDecider(T),
band: p ∧b q,
valueall-type: valueall-type(T),
bnot: ¬bb,
assert: ↑b,
ifthenelse: if b then t else f fi ,
isl: isl(x),
bool: 𝔹,
it: ⋅,
uimplies: b supposing a,
top: Top,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
unit: Unit,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
inr: inr x ,
inl: inl x,
union: left + right,
token: "$token",
universe: Type,
equal: s = t ∈ T,
record-select: r.x,
record+: record+,
record: record(x.T[x])
FDL editor aliases :
map-sig
map-sig\{i:l\}(Key;Value) ==
"map":\{m:Type| (valueall-type(m)) supposing (valueall-type(Value) and valueall-type(Key))\}
"eqKey":EqDecider(Key)
"find":Key {}\mrightarrow{} self."map" {}\mrightarrow{} (Value?)
"inDom":\{f:Key {}\mrightarrow{} self."map" {}\mrightarrow{} \mBbbB{}| \mforall{}k:Key. \mforall{}m:self."map". (\muparrow{}(f k m) \mLeftarrow{}{}\mRightarrow{} \muparrow{}isl(self."find" k m))\}
"empty":\{m:self."map"| \mforall{}k:Key. (\mneg{}\muparrow{}(self."inDom" k m))\}
"isEmpty":\{f:self."map" {}\mrightarrow{} \mBbbB{}| \mforall{}m:self."map". (\muparrow{}(f m) \mLeftarrow{}{}\mRightarrow{} \mforall{}k:Key. (\mneg{}\muparrow{}(self."inDom" k m)))\}
"update":\{f:Key {}\mrightarrow{} Value {}\mrightarrow{} self."map" {}\mrightarrow{} self."map"|
\mforall{}m:self."map". \mforall{}k1,k2:Key. \mforall{}v:Value.
((self."find" k1 (f k2 v m))
= if self."eqKey" k1 k2 then inl v else self."find" k1 m fi )\}
"add":\{f:Key {}\mrightarrow{} Value {}\mrightarrow{} self."map" {}\mrightarrow{} self."map"|
\mforall{}m:self."map". \mforall{}k1,k2:Key. \mforall{}v:Value.
((self."find" k1 (f k2 v m))
= if (self."eqKey" k1 k2) \mwedge{}\msubb{} (\mneg{}\msubb{}(self."inDom" k2 m))
then inl v
else self."find" k1 m
fi )\}
"remove":\{f:Key {}\mrightarrow{} self."map" {}\mrightarrow{} self."map"|
\mforall{}m:self."map". \mforall{}k1,k2:Key.
((self."find" k1 (f k2 m))
= if self."eqKey" k1 k2 then inr \mcdot{} else self."find" k1 m fi )\}
Date html generated:
2015_07_17-AM-08_21_59
Last ObjectModification:
2014_07_30-PM-02_34_34
Home
Index