OAI/Computability/WLIdentification/PresentationArithmetic.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WLIdentification.FinitePresentation.Number line 11
  2. structure OAI.WLIdentification.FinitePresentation.Test line 16
  3. abbrev OAI.WLIdentification.FinitePresentation.Map line 21
  4. theorem OAI.WLIdentification.FinitePresentation.Number.eval_poly line 27
  5. def OAI.WLIdentification.FinitePresentation.Number.congr line 32
  6. def OAI.WLIdentification.FinitePresentation.Number.code line 35
  7. def OAI.WLIdentification.FinitePresentation.Number.param line 38
  8. def OAI.WLIdentification.FinitePresentation.Number.const line 42
  9. def OAI.WLIdentification.FinitePresentation.Number.add line 44
  10. def OAI.WLIdentification.FinitePresentation.Number.mul line 46
  11. def OAI.WLIdentification.FinitePresentation.Number.sub line 48
  12. def OAI.WLIdentification.FinitePresentation.Number.pair line 50
  13. def OAI.WLIdentification.FinitePresentation.Number.mod line 52
  14. def OAI.WLIdentification.FinitePresentation.Number.div line 54
  15. def OAI.WLIdentification.FinitePresentation.Number.comp line 57
  16. theorem OAI.WLIdentification.FinitePresentation.Test.eval_poly line 67
  17. def OAI.WLIdentification.FinitePresentation.Test.congr line 72
  18. def OAI.WLIdentification.FinitePresentation.Test.const line 75
  19. def OAI.WLIdentification.FinitePresentation.Test.and line 78
  20. def OAI.WLIdentification.FinitePresentation.Test.or line 80
  21. def OAI.WLIdentification.FinitePresentation.Test.not line 82
  22. def OAI.WLIdentification.FinitePresentation.Test.numEq line 85
  23. def OAI.WLIdentification.FinitePresentation.Test.numLt line 87
  24. def OAI.WLIdentification.FinitePresentation.Test.comp line 90
  25. def OAI.WLIdentification.FinitePresentation.Number.ite line 100
  26. def OAI.WLIdentification.FinitePresentation.Map.id line 109
  27. def OAI.WLIdentification.FinitePresentation.Map.fst line 111
  28. def OAI.WLIdentification.FinitePresentation.Map.snd line 116
  29. def OAI.WLIdentification.FinitePresentation.Map.pair line 121
  30. def OAI.WLIdentification.FinitePresentation.Number.sumCases line 135
  31. def OAI.WLIdentification.FinitePresentation.Number.optionCases line 145
  32. def OAI.WLIdentification.FinitePresentation.Number.envelope line 155
  33. theorem OAI.WLIdentification.FinitePresentation.Number.lt_envelope line 158
  34. theorem OAI.WLIdentification.FinitePresentation.Number.envelope_poly line 163
  35. def OAI.WLIdentification.FinitePresentation.Presented.finSigma line 170
  36. def OAI.WLIdentification.FinitePresentation.Presented.restrict line 178
  37. def OAI.WLIdentification.FinitePresentation.Map.comp line 186
  38. def OAI.WLIdentification.FinitePresentation.Map.inl line 189
  39. def OAI.WLIdentification.FinitePresentation.Map.inr line 192
  40. def OAI.WLIdentification.FinitePresentation.Map.none line 195
  41. def OAI.WLIdentification.FinitePresentation.Map.some line 197
  42. def OAI.WLIdentification.FinitePresentation.Map.retype line 199
  43. def OAI.WLIdentification.FinitePresentation.Map.untype line 202
  44. def OAI.WLIdentification.FinitePresentation.Map.sigmaFst line 205
  45. def OAI.WLIdentification.FinitePresentation.Map.coe line 211
  46. def OAI.WLIdentification.FinitePresentation.Test.ite line 219
  47. def OAI.WLIdentification.FinitePresentation.Test.sumCases line 225
  48. def OAI.WLIdentification.FinitePresentation.Test.optionCases line 235
  49. def OAI.WLIdentification.FinitePresentation.Test.eq line 245
  50. theorem OAI.WLIdentification.WordExpressions.NatPoly.fixedTable line 255
  51. theorem OAI.WLIdentification.WordExpressions.BoolPoly.fixedTable line 272
  52. def OAI.WLIdentification.FinitePresentation.Presented.ofCode line 284
  53. def OAI.WLIdentification.FinitePresentation.Number.fixed line 306
  54. def OAI.WLIdentification.FinitePresentation.Test.fixed line 320