[Agda] Case split creates too many {_}
Apostolis Xekoukoulotakis
apostolis.xekoukoulotakis at gmail.com
Fri Apr 7 13:59:00 CEST 2017
```
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂
{lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) |
(drepl=>repl+ {frll = frll} ind lind)
... | g | r = {!!}
```
case splitting creates this:
```
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂
{lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) |
(drepl=>repl+ {frll = frll} ind lind)
removeCom {_} {_} {_} {_} {_} {frll} (_⊂_ {pll} {_} {_} {_} {ind} lf lf₁)
(_←⊂ {_} {_} {_} {_} {_} {_} {_} {lind} ic) | .(replLL _ (ind +ᵢ lind)
frll) | refl = ?
```
instead of :
```
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂
{lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) |
(drepl=>repl+ {frll = frll} ind lind)
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂
{lind = lind} ic) | .(replLL _ (ind +ᵢ lind) frll) | refl = ?
```
I wonder if the behavior can be changed.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170407/aae9925f/attachment.html>
More information about the Agda
mailing list