[Agda] agsy extensions

[Andreas Abel]

Not (yet) as far as I know. --Andreas

On 23.11.12 9:36 AM, Peter Divianszky wrote:
> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/