I think I&#39;ve suggested this before, but there&#39;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&#39;t know, you&#39;ll be able to click on symbols you don&#39;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">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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>
        _&lt;=_  extracted from this  ord,<br>
        ``with  x &lt;=? y&#39;&#39;   produced    no x-!&lt;=-y<br>
        (I think,   x-!&lt;=-y :  \neg x &lt;= y )<br>
<br>
(here I replace \&lt;= with &lt;= ).<br>
<br>
And from this   x-!&lt;=-y,  I need to construct  y&lt;=x : y &lt;= x.<br>
Because I think that this a constructive reifation for a classical<br>
lemma for  (Total &lt;=)  of that   not (x &lt;= y)  ==&gt;  y &lt;= x.<br>
I see in  Relation.Binary, Core:<br>
<br>
  record IsTotalOrder ...<br>
         isPartialOrder : IsPartialOrder _~~_ _&lt;=_<br>
         total          : Total _&lt;=_<br>
<br>
(here I replace some math symbols)<br>
<br>
  Total : forall {a l} {A : Set a} -&gt; Rel A l -&gt; Set _<br>
  Total _~_ = forall x y -&gt; (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 &lt;= x y :  (x &lt;= y) \u+ (y &lt;= x)<br>
and then to use                x-!&lt;=-y :  \neg x &lt;= y<br>
<br>
Where  \u+  is defined in the Standard library?<br>
It is visible a certain `combinator&#39;  &lt;\u+&gt;,  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 &lt;= y) includedInto (y &lt;= x)   for  _&lt;=_  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>