OAI/Combinatorics/EditApproximation/Geometry/InputViews.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Input intervals are views into the stored arrays. Their semantic lists are used by correctness statements; constructing a view stores only its two endpoints and does not materialize that list.

  1. structure OAI.EditApproximation.InputView line 11
  2. def OAI.EditApproximation.InputView.width line 21
  3. def OAI.EditApproximation.InputView.contents line 23
  4. theorem OAI.EditApproximation.InputView.contents_length line 25
  5. def OAI.EditApproximation.InputView.get line 28
  6. theorem OAI.EditApproximation.InputView.get_contents line 31
  7. def OAI.EditApproximation.InputView.whole line 35
  8. theorem OAI.EditApproximation.InputView.whole_contents line 37
  9. def OAI.EditApproximation.InputView.subview line 41
  10. theorem OAI.EditApproximation.InputView.subview_width line 49
  11. def OAI.EditApproximation.InputView.head? line 55

    Source documentation

    Reading a singleton view touches one stored array entry.

    def head? (view : InputView input) : Option α :=
…

    Mentions: OAI.EditApproximation.InputView

  12. theorem OAI.EditApproximation.InputView.head?_contents line 58