OAI/Computability/RationalHitting/ProcedurePairs.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.pairCode line 10

    Source documentation

    Serialization of a typed pair. Only the first field needs a delimiter.

    def pairCode {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (p : A×B) : List Bool :=
…
  2. lemma OAI.RationalHitting.StackLanguage.pairCode_length line 12
  3. def OAI.RationalHitting.StackLanguage.both line 16
  4. lemma OAI.RationalHitting.StackLanguage.both_first line 17
  5. lemma OAI.RationalHitting.StackLanguage.both_second line 19
  6. lemma OAI.RationalHitting.StackLanguage.both_comm line 20
  7. lemma OAI.RationalHitting.StackLanguage.both_nil_left line 22
  8. lemma OAI.RationalHitting.StackLanguage.both_nil_right line 24
  9. lemma OAI.RationalHitting.StackLanguage.extend_single_both line 27
  10. lemma OAI.RationalHitting.StackLanguage.Eval.rename_both line 41
  11. lemma OAI.RationalHitting.StackLanguage.eval_copy_single line 47
  12. def OAI.RationalHitting.StackLanguage.threeRegs line 55
  13. lemma OAI.RationalHitting.StackLanguage.threeRegs_inj line 56
  14. def OAI.RationalHitting.StackLanguage.prependRecord line 62

    Source documentation

    Prefix a record in its original order, consuming the first stack.

    def prependRecord (a b tmp : K) : Program K :=
…

    Mentions: OAI.RationalHitting.StackLanguage.Program

  15. lemma OAI.RationalHitting.StackLanguage.eval_prependRecord line 65
  16. lemma OAI.RationalHitting.StackLanguage.eval_prependRecord_both line 85
  17. def OAI.RationalHitting.StackLanguage.Procedure.pair line 98
  18. lemma OAI.RationalHitting.StackLanguage.eval_clear_both line 140
  19. lemma OAI.RationalHitting.StackLanguage.eval_reverse_both line 146
  20. lemma OAI.RationalHitting.StackLanguage.eval_reverse_single line 152
  21. lemma OAI.RationalHitting.StackLanguage.eval_clear_single line 156
  22. def OAI.RationalHitting.StackLanguage.pushWord line 162

    Source documentation

    A finite literal is written by a finite sequence; it is not a primitive which can materialize a word of unbounded length in one step.

    def pushWord (k : K) : List Bool → Program K
  | [] => .skip
  | b::w => .seq (pushWord k w) (.push k b)

    Mentions: OAI.RationalHitting.StackLanguage.Program

  23. lemma OAI.RationalHitting.StackLanguage.eval_pushWord line 165
  24. lemma OAI.RationalHitting.StackLanguage.eval_unpack_pair line 174
  25. def OAI.RationalHitting.StackLanguage.Procedure.const line 186
  26. def OAI.RationalHitting.StackLanguage.Procedure.fst line 200
  27. def OAI.RationalHitting.StackLanguage.Procedure.snd line 217
  28. def OAI.RationalHitting.StackLanguage.Procedure.appendWord line 233
  29. def OAI.RationalHitting.StackLanguage.Procedure.reverseWord line 250