OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryHeap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryMemoRawHeap line 11

   Source documentation

   Coarse words are borrowed from the separately allocated initializer. Every local buffer, guarded source read and final normalization is annotated.

   def computedQueryMemoRawHeap (source target : List ℕ) (N : ℕ)
       (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (input : ComputedFamilyInput source target N) (key : ComputedFamilyMemoKey source target N) :
       BitQuery.Heap (computedQueryMemoRaw source target N occurrence symbolBits positionBits input key) :=
   …

   Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyMemoKey, OAI.EditApproximation.BitQuery.Heap, OAI.EditApproximation.computedQueryMemoRaw

2. def OAI.EditApproximation.computedQueryMemoHeap line 26