2ed025ade8
This PR marks the automatically generated `sizeOf` theorems as `grind` theorems. closes #11259 Note: Requested update stage0, we need it to be able to solve example in the issue above. ```lean example (a: Nat) (b: Nat): sizeOf a < sizeOf (a, b) := by grind ``` |
||
|---|---|---|
| .. | ||
| src | ||
| stdlib | ||