OAI/Computability/SpaceSimulation/Binary.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Fifths.Bin.val line 12
  2. theorem OAI.Fifths.Bin.val_bits line 16
  3. def OAI.Fifths.Bin.esc line 21
  4. def OAI.Fifths.Bin.frame line 22
  5. theorem OAI.Fifths.Bin.frame_nil line 24
  6. theorem OAI.Fifths.Bin.frame_cons line 25
  7. def OAI.Fifths.Bin.pair line 28
  8. theorem OAI.Fifths.Bin.frameLength line 30
  9. theorem OAI.Fifths.Bin.bitTrue line 35
  10. theorem OAI.Fifths.Bin.frameBits line 38
  11. theorem OAI.Fifths.Bin.pair_bits line 50
  12. theorem OAI.Fifths.Bin.pair_ne_zero line 52
  13. theorem OAI.Fifths.Bin.pair_size line 53
  14. def OAI.Fifths.Bin.unpack line 58

    Source documentation

    Parse as a frame. Arbitrary result on malformed.

    def unpack : List Bool → List Bool × List Bool
  | false :: b :: l =>
    let (a,c) := unpack l
…
  15. theorem OAI.Fifths.Bin.unpack_frame line 65
  16. def OAI.Fifths.Bin.unpair line 70
  17. theorem OAI.Fifths.Bin.unpair_pair line 74
  18. theorem OAI.Fifths.Bin.pair_inj line 77
  19. theorem OAI.Fifths.Bin.mul_size line 83
  20. theorem OAI.Fifths.Bin.add_size line 87
  21. theorem OAI.Fifths.Bin.succ_size line 92
  22. theorem OAI.Fifths.Bin.pow_size line 97
  23. theorem OAI.Fifths.Bin.size_le_self line 105
  24. theorem OAI.Fifths.Bin.bits_nil line 110