OAI/Combinatorics/SnakyCertificate/Basic.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SnakyCertificate.rotationModulus_neZero line 7

    Also declared: ComparatorChallenges/SnakyCertificate.lean:7 (same declaration text).

  2. instance OAI.SnakyCertificate.digitModulus_neZero line 9

    Also declared: ComparatorChallenges/SnakyCertificate.lean:9 (same declaration text).

  3. abbrev OAI.SnakyCertificate.Cell line 11

    Also declared: ComparatorChallenges/SnakyCertificate.lean:11 (same declaration text).

  4. def OAI.SnakyCertificate.origin line 13

    Also declared: ComparatorChallenges/SnakyCertificate.lean:13 (same declaration text).

  5. def OAI.SnakyCertificate.snaky line 15

    Also declared: ComparatorChallenges/SnakyCertificate.lean:15 (same declaration text).

  6. def OAI.SnakyCertificate.orient line 17

    Also declared: ComparatorChallenges/SnakyCertificate.lean:17 (same declaration text).

  7. def OAI.SnakyCertificate.placement line 28

    Also declared: ComparatorChallenges/SnakyCertificate.lean:28 (same declaration text).

  8. def OAI.SnakyCertificate.basePoint line 30

    Also declared: ComparatorChallenges/SnakyCertificate.lean:30 (same declaration text).

  9. def OAI.SnakyCertificate.baseEnvelope line 32

    Also declared: ComparatorChallenges/SnakyCertificate.lean:32 (same declaration text).

  10. def OAI.SnakyCertificate.baseRequired line 35

    Also declared: ComparatorChallenges/SnakyCertificate.lean:35 (same declaration text).

  11. structure OAI.SnakyCertificate.Term line 37

    Also declared: ComparatorChallenges/SnakyCertificate.lean:37 (same declaration text).

  12. def OAI.SnakyCertificate.Term.shift line 44

    Also declared: ComparatorChallenges/SnakyCertificate.lean:44 (same declaration text).

  13. structure OAI.SnakyCertificate.Entry line 46

    Also declared: ComparatorChallenges/SnakyCertificate.lean:46 (same declaration text).

  14. def OAI.SnakyCertificate.emptyEntry line 51

    Also declared: ComparatorChallenges/SnakyCertificate.lean:51 (same declaration text).