1+ <!DOCTYPE HTML>
2+ < html > < head > < meta charset ="utf-8 "> < title > Data.List.Fresh.Membership.DecSetoid</ title > < link rel ="stylesheet " href ="Agda.css "> </ head > < body > < pre class ="Agda "> < a id ="1 " class ="Comment "> ------------------------------------------------------------------------</ a >
3+ < a id ="74 " class ="Comment "> -- The Agda standard library</ a >
4+ < a id ="103 " class ="Comment "> --</ a >
5+ < a id ="106 " class ="Comment "> -- Decidable setoid membership over fresh lists</ a >
6+ < a id ="154 " class ="Comment "> ------------------------------------------------------------------------</ a >
7+
8+ < a id ="228 " class ="Symbol "> {-#</ a > < a id ="232 " class ="Keyword "> OPTIONS</ a > < a id ="240 " class ="Pragma "> --cubical-compatible</ a > < a id ="261 " class ="Pragma "> --safe</ a > < a id ="268 " class ="Symbol "> #-}</ a >
9+
10+ < a id ="273 " class ="Keyword "> open</ a > < a id ="278 " class ="Keyword "> import</ a > < a id ="285 " href ="Relation.Binary.Bundles.html " class ="Module "> Relation.Binary.Bundles</ a > < a id ="309 " class ="Keyword "> using</ a > < a id ="315 " class ="Symbol "> (</ a > < a id ="316 " href ="Relation.Binary.Bundles.html#1703 " class ="Record "> DecSetoid</ a > < a id ="325 " class ="Symbol "> )</ a >
11+
12+ < a id ="328 " class ="Keyword "> module</ a > < a id ="335 " href ="Data.List.Fresh.Membership.DecSetoid.html " class ="Module "> Data.List.Fresh.Membership.DecSetoid</ a > < a id ="372 " class ="Symbol "> {</ a > < a id ="373 " href ="Data.List.Fresh.Membership.DecSetoid.html#373 " class ="Bound "> a</ a > < a id ="375 " href ="Data.List.Fresh.Membership.DecSetoid.html#375 " class ="Bound "> ℓ</ a > < a id ="376 " class ="Symbol "> }</ a > < a id ="378 " class ="Symbol "> (</ a > < a id ="379 " href ="Data.List.Fresh.Membership.DecSetoid.html#379 " class ="Bound "> DS</ a > < a id ="382 " class ="Symbol "> :</ a > < a id ="384 " href ="Relation.Binary.Bundles.html#1703 " class ="Record "> DecSetoid</ a > < a id ="394 " href ="Data.List.Fresh.Membership.DecSetoid.html#373 " class ="Bound "> a</ a > < a id ="396 " href ="Data.List.Fresh.Membership.DecSetoid.html#375 " class ="Bound "> ℓ</ a > < a id ="397 " class ="Symbol "> )</ a > < a id ="399 " class ="Keyword "> where</ a >
13+
14+ < a id ="406 " class ="Keyword "> open</ a > < a id ="411 " class ="Keyword "> import</ a > < a id ="418 " href ="Level.html " class ="Module "> Level</ a > < a id ="424 " class ="Keyword "> using</ a > < a id ="430 " class ="Symbol "> (</ a > < a id ="431 " href ="Agda.Primitive.html#742 " class ="Postulate "> Level</ a > < a id ="436 " class ="Symbol "> )</ a >
15+ < a id ="438 " class ="Keyword "> open</ a > < a id ="443 " class ="Keyword "> import</ a > < a id ="450 " href ="Data.List.Fresh.Relation.Unary.Any.html " class ="Module "> Data.List.Fresh.Relation.Unary.Any</ a > < a id ="485 " class ="Keyword "> using</ a > < a id ="491 " class ="Symbol "> (</ a > < a id ="492 " href ="Data.List.Fresh.Relation.Unary.Any.html#2511 " class ="Function "> any?</ a > < a id ="496 " class ="Symbol "> )</ a >
16+ < a id ="498 " class ="Keyword "> import</ a > < a id ="505 " href ="Data.List.Fresh.Membership.Setoid.html " class ="Module "> Data.List.Fresh.Membership.Setoid</ a > < a id ="539 " class ="Symbol "> as</ a > < a id ="542 " class ="Module "> MembershipSetoid</ a >
17+ < a id ="559 " class ="Keyword "> open</ a > < a id ="564 " class ="Keyword "> import</ a > < a id ="571 " href ="Relation.Binary.Core.html " class ="Module "> Relation.Binary.Core</ a > < a id ="592 " class ="Keyword "> using</ a > < a id ="598 " class ="Symbol "> (</ a > < a id ="599 " href ="Relation.Binary.Core.html#896 " class ="Function "> Rel</ a > < a id ="602 " class ="Symbol "> )</ a >
18+ < a id ="604 " class ="Keyword "> open</ a > < a id ="609 " class ="Keyword "> import</ a > < a id ="616 " href ="Relation.Binary.Definitions.html " class ="Module "> Relation.Binary.Definitions</ a > < a id ="644 " class ="Keyword "> using</ a > < a id ="650 " class ="Symbol "> (</ a > < a id ="651 " href ="Relation.Binary.Definitions.html#6907 " class ="Function "> Decidable</ a > < a id ="660 " class ="Symbol "> )</ a >
19+ < a id ="662 " class ="Keyword "> open</ a > < a id ="667 " class ="Keyword "> import</ a > < a id ="674 " href ="Relation.Nullary.Decidable.html " class ="Module "> Relation.Nullary.Decidable</ a > < a id ="701 " class ="Keyword "> using</ a > < a id ="707 " class ="Symbol "> (</ a > < a id ="708 " href ="Relation.Nullary.Decidable.Core.html#3274 " class ="Function "> ¬?</ a > < a id ="710 " class ="Symbol "> )</ a >
20+
21+ < a id ="713 " class ="Keyword "> open</ a > < a id ="718 " href ="Relation.Binary.Bundles.html#1703 " class ="Module "> DecSetoid</ a > < a id ="728 " href ="Data.List.Fresh.Membership.DecSetoid.html#379 " class ="Bound "> DS</ a > < a id ="731 " class ="Keyword "> using</ a > < a id ="737 " class ="Symbol "> (</ a > < a id ="738 " href ="Relation.Binary.Bundles.html#1958 " class ="Function "> setoid</ a > < a id ="744 " class ="Symbol "> ;</ a > < a id ="746 " href ="Relation.Binary.Structures.html#1994 " class ="Function Operator "> _≟_</ a > < a id ="749 " class ="Symbol "> )</ a > < a id ="751 " class ="Keyword "> renaming</ a > < a id ="760 " class ="Symbol "> (</ a > < a id ="761 " href ="Relation.Binary.Bundles.html#1769 " class ="Field "> Carrier</ a > < a id ="769 " class ="Symbol "> to</ a > < a id ="772 " class ="Field "> A</ a > < a id ="773 " class ="Symbol "> )</ a >
22+
23+ < a id ="776 " class ="Keyword "> private</ a >
24+ < a id ="786 " class ="Keyword "> variable</ a >
25+ < a id ="799 " href ="Data.List.Fresh.Membership.DecSetoid.html#799 " class ="Generalizable "> r</ a > < a id ="801 " class ="Symbol "> :</ a > < a id ="803 " href ="Agda.Primitive.html#742 " class ="Postulate "> Level</ a >
26+ < a id ="813 " href ="Data.List.Fresh.Membership.DecSetoid.html#813 " class ="Generalizable "> R</ a > < a id ="815 " class ="Symbol "> :</ a > < a id ="817 " href ="Relation.Binary.Core.html#896 " class ="Function "> Rel</ a > < a id ="821 " href ="Data.List.Fresh.Membership.DecSetoid.html#772 " class ="Field "> A</ a > < a id ="823 " href ="Data.List.Fresh.Membership.DecSetoid.html#799 " class ="Generalizable "> r</ a >
27+
28+
29+ < a id ="827 " class ="Comment "> ------------------------------------------------------------------------</ a >
30+ < a id ="900 " class ="Comment "> -- Re-export contents of Setoid membership</ a >
31+ < a id ="943 " class ="Keyword "> open</ a > < a id ="948 " href ="Data.List.Fresh.Membership.Setoid.html " class ="Module "> MembershipSetoid</ a > < a id ="965 " href ="Relation.Binary.Bundles.html#1958 " class ="Function "> setoid</ a > < a id ="972 " class ="Keyword "> public</ a >
32+
33+ < a id ="980 " class ="Comment "> ------------------------------------------------------------------------</ a >
34+ < a id ="1053 " class ="Comment "> -- Other operations</ a >
35+ < a id ="1073 " class ="Keyword "> infix</ a > < a id ="1079 " class ="Number "> 4</ a > < a id ="1081 " href ="Data.List.Fresh.Membership.DecSetoid.html#1092 " class ="Function Operator "> _∈?_</ a > < a id ="1086 " href ="Data.List.Fresh.Membership.DecSetoid.html#1149 " class ="Function Operator "> _∉?_</ a >
36+
37+ < a id ="_∈?_ "> </ a > < a id ="1092 " href ="Data.List.Fresh.Membership.DecSetoid.html#1092 " class ="Function Operator "> _∈?_</ a > < a id ="1097 " class ="Symbol "> :</ a > < a id ="1099 " href ="Relation.Binary.Definitions.html#6907 " class ="Function "> Decidable</ a > < a id ="1109 " class ="Symbol "> (</ a > < a id ="1110 " href ="Data.List.Fresh.Membership.Setoid.html#723 " class ="Function Operator "> _∈_</ a > < a id ="1114 " class ="Symbol "> {</ a > < a id ="1115 " class ="Argument "> R</ a > < a id ="1117 " class ="Symbol "> =</ a > < a id ="1119 " href ="Data.List.Fresh.Membership.DecSetoid.html#813 " class ="Generalizable "> R</ a > < a id ="1120 " class ="Symbol "> })</ a >
38+ < a id ="1123 " href ="Data.List.Fresh.Membership.DecSetoid.html#1123 " class ="Bound "> x</ a > < a id ="1125 " href ="Data.List.Fresh.Membership.DecSetoid.html#1092 " class ="Function Operator "> ∈?</ a > < a id ="1128 " href ="Data.List.Fresh.Membership.DecSetoid.html#1128 " class ="Bound "> xs</ a > < a id ="1131 " class ="Symbol "> =</ a > < a id ="1133 " href ="Data.List.Fresh.Relation.Unary.Any.html#2511 " class ="Function "> any?</ a > < a id ="1138 " class ="Symbol "> (</ a > < a id ="1139 " href ="Data.List.Fresh.Membership.DecSetoid.html#1123 " class ="Bound "> x</ a > < a id ="1141 " href ="Relation.Binary.Structures.html#1994 " class ="Function Operator "> ≟_</ a > < a id ="1143 " class ="Symbol "> )</ a > < a id ="1145 " href ="Data.List.Fresh.Membership.DecSetoid.html#1128 " class ="Bound "> xs</ a >
39+
40+ < a id ="_∉?_ "> </ a > < a id ="1149 " href ="Data.List.Fresh.Membership.DecSetoid.html#1149 " class ="Function Operator "> _∉?_</ a > < a id ="1154 " class ="Symbol "> :</ a > < a id ="1156 " href ="Relation.Binary.Definitions.html#6907 " class ="Function "> Decidable</ a > < a id ="1166 " class ="Symbol "> (</ a > < a id ="1167 " href ="Data.List.Fresh.Membership.Setoid.html#791 " class ="Function Operator "> _∉_</ a > < a id ="1171 " class ="Symbol "> {</ a > < a id ="1172 " class ="Argument "> R</ a > < a id ="1174 " class ="Symbol "> =</ a > < a id ="1176 " href ="Data.List.Fresh.Membership.DecSetoid.html#813 " class ="Generalizable "> R</ a > < a id ="1177 " class ="Symbol "> })</ a >
41+ < a id ="1180 " href ="Data.List.Fresh.Membership.DecSetoid.html#1180 " class ="Bound "> x</ a > < a id ="1182 " href ="Data.List.Fresh.Membership.DecSetoid.html#1149 " class ="Function Operator "> ∉?</ a > < a id ="1185 " href ="Data.List.Fresh.Membership.DecSetoid.html#1185 " class ="Bound "> xs</ a > < a id ="1188 " class ="Symbol "> =</ a > < a id ="1190 " href ="Relation.Nullary.Decidable.Core.html#3274 " class ="Function "> ¬?</ a > < a id ="1193 " class ="Symbol "> (</ a > < a id ="1194 " href ="Data.List.Fresh.Membership.DecSetoid.html#1180 " class ="Bound "> x</ a > < a id ="1196 " href ="Data.List.Fresh.Membership.DecSetoid.html#1092 " class ="Function Operator "> ∈?</ a > < a id ="1199 " href ="Data.List.Fresh.Membership.DecSetoid.html#1185 " class ="Bound "> xs</ a > < a id ="1201 " class ="Symbol "> )</ a >
42+ </ pre > </ body > </ html >
![github-merge-queue[bot]](https://avatars.githubusercontent.com/u/9919?v=4&size=40){kind=avatar}
0 commit comments