0173444d24
This PR implements heterogeneous contructor injectivity in `grind`. Example: ```lean opaque double : Nat → Nat inductive Parity : Nat -> Type | even (n) : Parity (double n) | odd (n) : Parity (Nat.succ (double n)) opaque q : Nat → Nat → Prop axiom qax : q a b → double a = double b attribute [grind →] qax example (motive : (x : Nat) → Parity x → Sort u_1) (h_2 : (j : Nat) → motive (double j) (Parity.even j)) (j n : Nat) (heq_1 : q j n) -- Implies that `double j = double n` (heq_2 : Parity.even n ≍ Parity.even j): h_2 n ≍ h_2 j := by grind ``` Closes #11449 |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||