OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryAnswer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryAnswerWithWork line 11

   Source documentation

   Binary output conversion, with the explicit equal-string guard.

   def computedQueryAnswerWithWork (source target : List ℕ) (N : ℕ)
       (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ)
       (input : ComputedFamilyInput source target N) : List Bool × ℕ :=
   …

   Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.ComputedFamilyInput

2. theorem OAI.EditApproximation.computedQueryAnswerWithWork_value line 19
3. theorem OAI.EditApproximation.computedQueryAnswerWithWork_cost line 41