OAI/Combinatorics/SumProduct/Alignment/IntegerArrays01.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceIntegerArrays.rSlot line 17
  2. def OAI.SourceIntegerArrays.offset0 line 20
  3. def OAI.SourceIntegerArrays.offset1 line 23
  4. def OAI.SourceIntegerArrays.exponent line 27
  5. lemma OAI.SourceIntegerArrays.rSlot_expose line 41
  6. lemma OAI.SourceIntegerArrays.shift_mul line 52
  7. lemma OAI.SourceIntegerArrays.slot_numerator_div line 68
  8. lemma OAI.SourceIntegerArrays.exponent_cast line 86
  9. theorem OAI.SourceIntegerArrays.source_integer_array_evaluation line 169
  10. def OAI.SourceIntegerArrays.literalState line 210
  11. theorem OAI.SourceIntegerArrays.source_literal_entire_array line 234