3cde12567f
This PR adds a `HPow \a Int \a` field to `Lean.Grind.Field`, and sufficient axioms to connect it to the operations, so that in future we can reason about exponents in `grind`. To avoid collisions, we also move the `HPow \a Nat \a` field in `Semiring` from the extends clause to a field. Finally, we add some failing tests about normalizing exponents. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Envelope.lean | ||
| Field.lean | ||
| OfSemiring.lean | ||
| Poly.lean | ||
| ToInt.lean | ||