OAI/Combinatorics/LowSpaceSubsetSum/Storage/StoredEntry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LowSpaceSubsetSum.StoredEntry line 10
2. def OAI.LowSpaceSubsetSum.StoredEntry.semantic line 18
3. def OAI.LowSpaceSubsetSum.StoredEntry.encode line 20
4. theorem OAI.LowSpaceSubsetSum.StoredEntry.encode_value line 23
5. theorem OAI.LowSpaceSubsetSum.StoredEntry.encode_width line 27
6. theorem OAI.LowSpaceSubsetSum.StoredEntry.encode_work line 31
7. def OAI.LowSpaceSubsetSum.StoredEntry.cells line 36

   Source documentation

   One scalar and the mask list, including its pointer/header.

   def cells (x : StoredEntry n) : ℕ := x.mask.indices.length + 2

   Mentions: OAI.LowSpaceSubsetSum.StoredEntry

8. theorem OAI.LowSpaceSubsetSum.StoredEntry.cells_le line 38
9. abbrev OAI.LowSpaceSubsetSum.StoredEntry.Dictionary line 42
10. def OAI.LowSpaceSubsetSum.StoredEntry.empty line 45
11. def OAI.LowSpaceSubsetSum.StoredEntry.report line 48
12. theorem OAI.LowSpaceSubsetSum.StoredEntry.report_work line 53
13. def OAI.LowSpaceSubsetSum.StoredEntry.mapDictionary line 63

    Source documentation

    Erase bounded-list records while keeping the same trie and array order.

    def mapDictionary (r : RecordedDictionary.State (StoredEntry n)) :
        RecordedDictionary.State (Entry (Fin n)) :=
    …

    Mentions: OAI.LowSpaceSubsetSum.RecordedDictionary.State, OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.Entry

14. theorem OAI.LowSpaceSubsetSum.StoredEntry.mapDictionary_feed line 67
15. theorem OAI.LowSpaceSubsetSum.StoredEntry.report_value line 78