OAI/Combinatorics/MatchingCount/Sampling/TreeUnitSampler.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.ExecutableUnit.Bits line 10
  2. abbrev OAI.MatchingFPRAS.ExecutableUnit.State line 11
  3. def OAI.MatchingFPRAS.ExecutableUnit.nextContext line 12
  4. def OAI.MatchingFPRAS.ExecutableUnit.nextContextRealizer line 14
  5. def OAI.MatchingFPRAS.ExecutableUnit.selected line 16
  6. def OAI.MatchingFPRAS.ExecutableUnit.selectedRealizer line 17
  7. def OAI.MatchingFPRAS.ExecutableUnit.step line 20
  8. def OAI.MatchingFPRAS.ExecutableUnit.stepRealizer line 25
  9. def OAI.MatchingFPRAS.ExecutableUnit.rawSample line 35
  10. def OAI.MatchingFPRAS.ExecutableUnit.unwind line 41
  11. lemma OAI.MatchingFPRAS.ExecutableUnit.descend_unwind line 42
  12. def OAI.MatchingFPRAS.ExecutableUnit.sample line 60
  13. def OAI.MatchingFPRAS.ExecutableUnit.sampleRealizer line 61
  14. lemma OAI.MatchingFPRAS.ExecutableUnit.selected_eq_of_getD line 69