OAI/Combinatorics/ThinTrees/Arithmetic/BoolPrograms.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Bool programs.

  1. def OAI.CurrentKS.Realization.Realizes.or line 14
  2. instance OAI.CurrentKS.Realization.poly_or line 19
  3. abbrev OAI.CurrentKS.Realization.boolsCode line 24
  4. def OAI.CurrentKS.Realization.anyTrue line 26
  5. instance OAI.CurrentKS.Realization.poly_anyTrue line 32
  6. def OAI.CurrentKS.Realization.allTrue line 34
  7. instance OAI.CurrentKS.Realization.poly_allTrue line 39
  8. def OAI.CurrentKS.Realization.Realizes.existsFin line 42
  9. instance OAI.CurrentKS.Realization.poly_existsFin line 47
  10. def OAI.CurrentKS.Realization.Realizes.forallFin line 52
  11. instance OAI.CurrentKS.Realization.poly_forallFin line 57
  12. lemma OAI.CurrentKS.Realization.bools_length line 62
  13. lemma OAI.CurrentKS.Realization.bools_ofFn_length line 71