Mimer doesn't fill with simplified solution

[leoydm]

In Agda master-32724f0, Mimer fills the second example with refl (map (_+_ 1) []). Expect both holes to be filled with refl [] as Agsy does in Agda v2.6.4.3.

open import Agda.Builtin.List
open import Agda.Builtin.Nat

map : {X Y : Set} → (X → Y) → List X → List Y
map f []        = []
map f (x ∷ xs)  = f x ∷ map f xs

data _≡_ {A : Set} : A → A → Set where
  refl : (x : A) → x ≡ x

example1 : [] ≡ map (1 +_) []
example1 = {!!}     -- Mimer fills with "refl []"

example2 : map (1 +_) [] ≡ []
example2 = {!!}     -- Mimer fills with "refl (map (_+_ 1) [])"

[gallais]

Can you not get the normalised result by prefixing with C-u C-u? It may better not to do arbitrary normalisation unless the user requests it explicitly.

[leoydm]

Can you not get the normalised result by prefixing with C-u C-u? It may better not to do arbitrary normalisation unless the user requests it explicitly.

I did try C-u C-u C-c C-a and it still gave me refl (map (_+_ 1) []). Today I tested with the latest commit 691b30a and it behaves the same.

[andreasabel]

Proposed fix: support the simplify/normalise prefix C-u ... also for Mimer.