f64753c106
We don't want to avoid proofs at `List.getIdx` and `Expr` when doing proofs by reflection. The new encoding avoids that by using the fact that `vars` in `Context` should never be empty. To be honest, the best approach is still the old `unit`. We can just rename it to `inhabitant` to make sure users don't assume it is the unit of the AC operator. Then, we can just set it with the first element of `vars` and avoid proofs at `denote`. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| leanpkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||