I think I've suggested this before, but there's super hyperlinked documentation online at <a href="http://www.cse.chalmers.se/~nad/listings/lib/Everything.html#1">http://www.cse.chalmers.se/~nad/listings/lib/Everything.html#1</a>, so if you navigate to a module that references something you don't know, you'll be able to click on symbols you don't recognize (like \u+) and it will take you to their definitions.<div>
<br></div><div>Another option to search is simply to type \u+ into Agda-mode, take the symbol it gives you, paste that into grep, and grep anyway.<br><br><div class="gmail_quote">On Wed, Oct 10, 2012 at 11:59 AM, Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I have a beginner question on usage of DecTotalOrder of Standard<br>
library.<br>
<br>
I have ord : DecTotalOrder,<br>
_<=_ extracted from this ord,<br>
``with x <=? y'' produced no x-!<=-y<br>
(I think, x-!<=-y : \neg x <= y )<br>
<br>
(here I replace \<= with <= ).<br>
<br>
And from this x-!<=-y, I need to construct y<=x : y <= x.<br>
Because I think that this a constructive reifation for a classical<br>
lemma for (Total <=) of that not (x <= y) ==> y <= x.<br>
I see in Relation.Binary, Core:<br>
<br>
record IsTotalOrder ...<br>
isPartialOrder : IsPartialOrder _~~_ _<=_<br>
total : Total _<=_<br>
<br>
(here I replace some math symbols)<br>
<br>
Total : forall {a l} {A : Set a} -> Rel A l -> Set _<br>
Total _~_ = forall x y -> (x ~ y) \u+ (y ~ x)<br>
<br>
, where \u+ denotes, I think, something close to union of types.<br>
How to operate with a data from (P \u+ Q) ?<br>
what are the constructors?<br>
Probably, one needs to apply total <= x y : (x <= y) \u+ (y <= x)<br>
and then to use x-!<=-y : \neg x <= y<br>
<br>
Where \u+ is defined in the Standard library?<br>
It is visible a certain `combinator' <\u+>, with the denotation<br>
[ P , Q ]. I do not know of what does all this mean.<br>
<br>
If it was not a math symbol, I could apply grep foo *.agda.<br>
<br>
May be, Standard Library provides somewhere a lemma, like<br>
<br>
(\neg x <= y) includedInto (y <= x) for _<=_ from TotalOrder ?<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>