[Agda] agsy extensions

[Peter Divianszky]

Hi,

Is there a way to extend Agsy?

I defined a permutation relation _~_ and a function

_~?_ : ∀ xs ys → Dec (xs ~ ys)

I was also able to define 'solvePerm' such that the Agda accepts

x : 1 ∷ 2 ∷ 2 ∷ 4 ∷ 5 ∷ [] ~ 2 ∷ 2 ∷ 1 ∷ 4 ∷ 5 ∷ []
x = quoteGoal t in solvePerm t

y : ¬ (1 ∷ 1 ∷ 2 ∷ 4 ∷ 5 ∷ [] ~ 2 ∷ 2 ∷ 1 ∷ 4 ∷ 5 ∷ [])
y = quoteGoal t in solvePerm t

Is it possible to extend Agsy from an .agda module such that the auto 
command C-c C-a would fill the hole?

x : 1 ∷ 2 ∷ 2 ∷ 4 ∷ 5 ∷ [] ~ 2 ∷ 2 ∷ 1 ∷ 4 ∷ 5 ∷ []
x = {! !}

Thanks,
Peter