OAI/Computability/SpaceSimulation/Register/Digits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Little-endian packed buffers.

  1. def OAI.Fifths.Radix.pack line 9
  2. def OAI.Fifths.Radix.get line 13
  3. theorem OAI.Fifths.Radix.get_lt line 15
  4. theorem OAI.Fifths.Radix.get_zero line 17
  5. theorem OAI.Fifths.Radix.get_succ line 18
  6. theorem OAI.Fifths.Radix.pack_lt line 21
  7. theorem OAI.Fifths.Radix.pack_cons line 34
  8. theorem OAI.Fifths.Radix.get_pack line 42
  9. theorem OAI.Fifths.Radix.pack_get line 59
  10. theorem OAI.Fifths.Radix.pack_congr line 69
  11. theorem OAI.Fifths.Radix.ext line 75
  12. theorem OAI.Fifths.Comp.digit line 86

    Source documentation

    Supplied powers of a computable base are computable when the resulting integer fits.

    theorem digit (p : Comp x S a m) (q : Comp x S a u) (h : Comp x S a b)
    (l : Fits S (fun i => m i ^ b i)) :
    Comp x S a (fun i => get (m i) (u i) (b i)) :=
…

    Mentions: OAI.Fifths.Comp, OAI.Fifths.Fits

  13. theorem OAI.Fifths.Comp.digits line 91