OAI/Analysis/MatrixSigning/Realization/SearchRealization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentKS.Realization.SearchState line 13
  2. def OAI.CurrentKS.Realization.searchStateData line 21
  3. def OAI.CurrentKS.Realization.searchStateCode line 23
  4. def OAI.CurrentKS.Realization.searchView line 24
  5. def OAI.CurrentKS.Realization.searchPencil line 26
  6. def OAI.CurrentKS.Realization.searchParameters line 28
  7. def OAI.CurrentKS.Realization.searchY line 31
  8. def OAI.CurrentKS.Realization.searchDim line 34
  9. def OAI.CurrentKS.Realization.searchStepRealizes line 36
  10. def OAI.CurrentKS.Realization.searchMeshRealizes line 40
  11. def OAI.CurrentKS.Realization.searchFuelRealizes line 47
  12. def OAI.CurrentKS.Realization.SearchState.init line 53
  13. def OAI.CurrentKS.Realization.searchInit line 55
  14. lemma OAI.CurrentKS.Realization.pencilNext_iterate line 59
  15. def OAI.CurrentKS.Realization.search line 65