diff options
| author | Pierre-Marie Pédrot | 2020-03-20 15:28:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-20 15:53:57 +0100 |
| commit | c64a18bcdd0489586f8ff386f7daa432f7229407 (patch) | |
| tree | bf770ffd2f006f65cfba3615108f3cf77883643d /dev/ci/ci-basic-overlay.sh | |
| parent | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (diff) | |
Fix the computation of recursive principles with let-bindings.
We use a more robust implementation that does not assume that the type
of the inductive is in ζ-normal form. This code path is not exercised,
because due to the kernel typing algorithm, let-bindings in the type
of a recursor are expanded away.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions