[Agda] Re: C-style macros in Agda :)
Andreas Abel
andreas.abel at ifi.lmu.de
Sun Feb 3 19:27:09 CET 2013
Well you can always use the C preprocessor, but then you are restricted
to batch-mode Agda. Which isn't what you want, I suppose.
Did you try the 'syntax' facility? (Might not work...)
Default arguments or eta-expansion for the propositional equality might
help you, but these are not or not yet in Agda.
Cheers,
Andreas
On 02.02.13 11:51 AM, Dmytro Starosud wrote:
> I might be not clear enough.
> Could you please refer to this
> (https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda).
> I want to get rid of:
>
> ⇒⟦ refl ⟧⇒
>
> e.g. replace it with "then", which would mean semicolon just like in
> imperative program
>
> Best regards,
> Dmytro
>
> 2013/2/1 Dmytro Starosud <d.starosud at gmail.com
> <mailto:d.starosud at gmail.com>>
>
> Hello list,
>
> I have the following code (simplified).
>
> A B : Set
>
> Ty : Set → Set → Set
> op : Set → Set
>
> f : ∀ {A B} → op A ≡ op B → Ty A B → Ty B A
> x : Ty A B
>
> y = f refl x
>
> I should always write "f refl", because A and B is known at compile
> time and if "op A ≡ op B" is inhabited then "refl" is enough, I mean
> I don't need to write complex proof.
> But "op B : Set" is undecidable, so I cannot make that proof
> implicit, and also I cannot make it inferable (Agda not always wants
> to infer "refl" even if "op A" is exactly the same as "op B").
>
> Is there any way to substitute "f refl" with some "g"? I mean
> something like C-style macros:
> #define g (f refl)
>
> Thanks in advance,
> Dmytro
>
>
>
>
> _______________________________________________
> 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/
More information about the Agda
mailing list