/usr/share/doc/agda-stdlib-doc/html/Agda.Builtin.TrustMe.html is in agda-stdlib-doc 0.12-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 | <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml"
><head
><title
>Agda.Builtin.TrustMe</title
><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
/><meta http-equiv="Content-Style-Type" content="text/css"
/><link href="Agda.css" rel="stylesheet" type="text/css"
/></head
><body
><pre
><a name="1"
>
</a
><a name="2" class="Keyword"
>module</a
><a name="8"
> </a
><a name="9" href="Agda.Builtin.TrustMe.html#1" class="Module"
>Agda.Builtin.TrustMe</a
><a name="29"
> </a
><a name="30" class="Keyword"
>where</a
><a name="35"
>
</a
><a name="37" class="Keyword"
>open</a
><a name="41"
> </a
><a name="42" class="Keyword"
>import</a
><a name="48"
> </a
><a name="49" href="Agda.Builtin.Equality.html#1" class="Module"
>Agda.Builtin.Equality</a
><a name="70"
>
</a
><a name="72" class="Keyword"
>primitive</a
><a name="81"
> </a
><a name="82" href="Agda.Builtin.TrustMe.html#82" class="Primitive"
>primTrustMe</a
><a name="93"
> </a
><a name="94" class="Symbol"
>:</a
><a name="95"
> </a
><a name="96" class="Symbol"
>∀</a
><a name="97"
> </a
><a name="98" class="Symbol"
>{</a
><a name="99" href="Agda.Builtin.TrustMe.html#99" class="Bound"
>a</a
><a name="100" class="Symbol"
>}</a
><a name="101"
> </a
><a name="102" class="Symbol"
>{</a
><a name="103" href="Agda.Builtin.TrustMe.html#103" class="Bound"
>A</a
><a name="104"
> </a
><a name="105" class="Symbol"
>:</a
><a name="106"
> </a
><a name="107" class="PrimitiveType"
>Set</a
><a name="110"
> </a
><a name="111" href="Agda.Builtin.TrustMe.html#99" class="Bound"
>a</a
><a name="112" class="Symbol"
>}</a
><a name="113"
> </a
><a name="114" class="Symbol"
>{</a
><a name="115" href="Agda.Builtin.TrustMe.html#115" class="Bound"
>x</a
><a name="116"
> </a
><a name="117" href="Agda.Builtin.TrustMe.html#117" class="Bound"
>y</a
><a name="118"
> </a
><a name="119" class="Symbol"
>:</a
><a name="120"
> </a
><a name="121" href="Agda.Builtin.TrustMe.html#103" class="Bound"
>A</a
><a name="122" class="Symbol"
>}</a
><a name="123"
> </a
><a name="124" class="Symbol"
>→</a
><a name="125"
> </a
><a name="126" href="Agda.Builtin.TrustMe.html#115" class="Bound"
>x</a
><a name="127"
> </a
><a name="128" href="Agda.Builtin.Equality.html#55" class="Datatype Operator"
>≡</a
><a name="129"
> </a
><a name="130" href="Agda.Builtin.TrustMe.html#117" class="Bound"
>y</a
><a name="131"
>
</a
></pre
></body
></html
>
|