@dselsam You have used a function similar to prove_eq_rec_invertible in the inductive compiler. I'm wondering if this bug (missing case) may also occur in the inductive compiler. |
||
|---|---|---|
| .. | ||
| lean | ||
| .gitignore | ||
@dselsam You have used a function similar to prove_eq_rec_invertible in the inductive compiler. I'm wondering if this bug (missing case) may also occur in the inductive compiler. |
||
|---|---|---|
| .. | ||
| lean | ||
| .gitignore | ||