[Agda] Re: C-style macros in Agda :)

[Andreas Abel]

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/