[Agda] L and inverted L characters

Philippe de Rochambeau phiroc at free.fr
Tue Apr 14 21:48:35 CEST 2020


Unfortunately, the character can’t be copied from the paper, but thanks for the tip.

> Le 14 avr. 2020 à 21:47, a.j.rouvoet <a.j.rouvoet at gmail.com> a écrit :
> 
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda



More information about the Agda mailing list