[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