This file is indexed.

/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"
      >&#8704;</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"
      >&#8594;</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"
      >&#8801;</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
>