[Agda] L and inverted L characters

a.j.rouvoet a.j.rouvoet at gmail.com
Tue Apr 14 21:47:29 CEST 2020


In general, if you have a way to copy-paste the character into emacs, 
then you can ask emacs how to input it with describe-char.

Arjen

On 4/14/20 9:45 PM, Andreas Abel wrote:
> You mean \lfloor and \rfloor ?  (Just like in LaTeX.)
>
> On 2020-04-14 21:20, Philippe de Rochambeau wrote:
>> Hello,
>> in a paper entitled « The Power of Pi », the authors use two 
>> characters that look like a capital L and an inverted capital L, 
>> respectively.
>> Are these characters still used in Agda 2.6? If so, what are their 
>> names and how do you input them in Emacs?
>> Many thanks.
>> Cheers,
>> Philippe
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


More information about the Agda mailing list