This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.
File contents: Verification of associative lists
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getEntry? a [] = none
- Std.Internal.List.getEntry? a (⟨k, v⟩ :: l) = bif k == a then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getValue? a [] = none
- Std.Internal.List.getValue? a (⟨k, v⟩ :: l) = bif k == a then some v else Std.Internal.List.getValue? a l
Instances For
Internal implementation detail of the hash map
Equations
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.containsKey a [] = false
- Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = (k == a || Std.Internal.List.containsKey a l)
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getEntry a l h = (Std.Internal.List.getEntry? a l).get ⋯
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getValue a l h = (Std.Internal.List.getValue? a l).get ⋯
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getValueCast a l h = (Std.Internal.List.getValueCast? a l).get ⋯
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getValueCastD a l fallback = (Std.Internal.List.getValueCast? a l).getD fallback
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getValueD a l fallback = (Std.Internal.List.getValue? a l).getD fallback
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getKey? a [] = none
- Std.Internal.List.getKey? a (⟨k, v⟩ :: l) = bif k == a then some k else Std.Internal.List.getKey? a l
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getKey a l h = (Std.Internal.List.getKey? a l).get ⋯
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.getKeyD a l fallback = (Std.Internal.List.getKey? a l).getD fallback
Instances For
Internal implementation detail of the hash map
Equations
Instances For
Internal implementation detail of the hash map
Equations
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.insertEntry k v l = bif Std.Internal.List.containsKey k l then Std.Internal.List.replaceEntry k v l else ⟨k, v⟩ :: l
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.insertEntryIfNew k v l = bif Std.Internal.List.containsKey k l then l else ⟨k, v⟩ :: l
Instances For
This is a restatement of containsKey_insertEntryIfNew
that is written to exactly match the proof
obligation in the statement of getValueCast_insertEntryIfNew
.
Internal implementation detail of the hash map
Equations
- Std.Internal.List.insertList l [] = l
- Std.Internal.List.insertList l (⟨k, v⟩ :: l_1) = Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) l_1
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.insertListConst l toInsert = Std.Internal.List.insertList l (List.map Std.Internal.List.Prod.toSigma toInsert)
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.alterKey k f l = match f (Std.Internal.List.getValueCast? k l) with | none => Std.Internal.List.eraseKey k l | some v => Std.Internal.List.insertEntry k v l
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.Const.alterKey k f l = match f (Std.Internal.List.getValue? k l) with | none => Std.Internal.List.eraseKey k l | some v => Std.Internal.List.insertEntry k v l
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.modifyKey k f l = match Std.Internal.List.getValueCast? k l with | none => l | some v => Std.Internal.List.replaceEntry k (f v) l
Instances For
Internal implementation detail of the hash map
Equations
- Std.Internal.List.Const.modifyKey k f l = match Std.Internal.List.getValue? k l with | none => l | some v => Std.Internal.List.replaceEntry k (f v) l
Instances For
Given a proof that the list is nonempty, returns the smallest key in an associative list.
Equations
- Std.Internal.List.minKey xs h = (Std.Internal.List.minKey? xs).get ⋯
Instances For
Returns the smallest key in an associative list or fallback
if the list is empty.
Equations
- Std.Internal.List.minKeyD xs fallback = (Std.Internal.List.minKey? xs).getD fallback
Instances For
Returns the smallest key in an associative list or fallback
if the list is empty.
Equations
- Std.Internal.List.maxKeyD xs fallback = Std.Internal.List.minKeyD xs fallback