[Agda] Case split creates too many {_}

[Andreas Abel]

Agda uses {_} to skip unsupplied hidden arguments.  Instead it could use 
a named hidden argument for the supplied one {frll}.

Could you put a reasonably small self-contained test case on the issue 
tracker?

Thanks,
Andreas

On 07.04.2017 13:59, Apostolis Xekoukoulotakis wrote:
> ```
> 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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/