/usr/share/doc/agda-stdlib-doc/html/Data.Vec.Equality.html is in agda-stdlib-doc 0.14-1.
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 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Vec.Equality</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Semi-heterogeneous vector equality</a>
<a id="144" class="Comment">------------------------------------------------------------------------</a>
<a id="218" class="Keyword">module</a> <a id="225" href="Data.Vec.Equality.html" class="Module">Data.Vec.Equality</a> <a id="243" class="Keyword">where</a>
<a id="250" class="Keyword">open</a> <a id="255" class="Keyword">import</a> <a id="262" href="Data.Vec.html" class="Module">Data.Vec</a>
<a id="271" class="Keyword">open</a> <a id="276" class="Keyword">import</a> <a id="283" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="297" class="Keyword">using</a> <a id="303" class="Symbol">(</a><a id="304" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a><a id="307" class="Symbol">)</a>
<a id="309" class="Keyword">open</a> <a id="314" class="Keyword">import</a> <a id="321" href="Function.html" class="Module">Function</a>
<a id="330" class="Keyword">open</a> <a id="335" class="Keyword">import</a> <a id="342" href="Level.html" class="Module">Level</a> <a id="348" class="Keyword">using</a> <a id="354" class="Symbol">(</a><a id="355" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">_⊔_</a><a id="358" class="Symbol">)</a>
<a id="360" class="Keyword">open</a> <a id="365" class="Keyword">import</a> <a id="372" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="388" class="Keyword">open</a> <a id="393" class="Keyword">import</a> <a id="400" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="438" class="Symbol">as</a> <a id="441" class="Module">P</a> <a id="443" class="Keyword">using</a> <a id="449" class="Symbol">(</a><a id="450" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">_≡_</a><a id="453" class="Symbol">)</a>
<a id="455" class="Keyword">open</a> <a id="460" class="Keyword">import</a> <a id="467" href="Relation.Binary.HeterogeneousEquality.html" class="Module">Relation.Binary.HeterogeneousEquality</a> <a id="505" class="Symbol">as</a> <a id="508" class="Module">H</a> <a id="510" class="Keyword">using</a> <a id="516" class="Symbol">(</a><a id="517" href="Relation.Binary.HeterogeneousEquality.Core.html#_%E2%89%85_" class="Datatype Operator">_≅_</a><a id="520" class="Symbol">)</a>
<a id="522" class="Keyword">module</a> <a id="Equality" href="Data.Vec.Equality.html#Equality" class="Module">Equality</a> <a id="538" class="Symbol">{</a><a id="539" href="Data.Vec.Equality.html#539" class="Bound">s₁</a> <a id="542" href="Data.Vec.Equality.html#542" class="Bound">s₂</a><a id="544" class="Symbol">}</a> <a id="546" class="Symbol">(</a><a id="547" href="Data.Vec.Equality.html#547" class="Bound">S</a> <a id="549" class="Symbol">:</a> <a id="551" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="558" href="Data.Vec.Equality.html#539" class="Bound">s₁</a> <a id="561" href="Data.Vec.Equality.html#542" class="Bound">s₂</a><a id="563" class="Symbol">)</a> <a id="565" class="Keyword">where</a>
<a id="574" class="Keyword">private</a>
<a id="586" class="Keyword">open</a> <a id="591" class="Keyword">module</a> <a id="SS" href="Data.Vec.Equality.html#SS" class="Module">SS</a> <a id="601" class="Symbol">=</a> <a id="603" href="Relation.Binary.html#Setoid" class="Module">Setoid</a> <a id="610" href="Data.Vec.Equality.html#547" class="Bound">S</a>
<a id="618" class="Keyword">using</a> <a id="624" class="Symbol">()</a> <a id="627" class="Keyword">renaming</a> <a id="636" class="Symbol">(</a><a id="637" href="Relation.Binary.html#Equality.Equality.SS._%E2%89%88_" class="Field Operator">_≈_</a> <a id="641" class="Symbol">to</a> <a id="644" href="Relation.Binary.html#Equality.Equality.SS._%E2%89%88_" class="Field Operator">_≊_</a><a id="647" class="Symbol">;</a> <a id="649" href="Relation.Binary.html#Equality.Equality.SS.Carrier" class="Field">Carrier</a> <a id="657" class="Symbol">to</a> <a id="660" href="Relation.Binary.html#Equality.Equality.SS.Carrier" class="Field">A</a><a id="661" class="Symbol">)</a>
<a id="666" class="Keyword">infix</a> <a id="672" class="Number">4</a> <a id="674" href="Data.Vec.Equality.html#686" class="Datatype Operator">_≈_</a>
<a id="681" class="Keyword">data</a> <a id="Equality._≈_" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">_≈_</a> <a id="690" class="Symbol">:</a> <a id="692" class="Symbol">∀</a> <a id="694" class="Symbol">{</a><a id="695" href="Data.Vec.Equality.html#695" class="Bound">n¹</a><a id="697" class="Symbol">}</a> <a id="699" class="Symbol">→</a> <a id="701" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="705" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="707" href="Data.Vec.Equality.html#695" class="Bound">n¹</a> <a id="710" class="Symbol">→</a>
<a id="725" class="Symbol">∀</a> <a id="727" class="Symbol">{</a><a id="728" href="Data.Vec.Equality.html#728" class="Bound">n²</a><a id="730" class="Symbol">}</a> <a id="732" class="Symbol">→</a> <a id="734" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="738" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="740" href="Data.Vec.Equality.html#728" class="Bound">n²</a> <a id="743" class="Symbol">→</a> <a id="745" class="PrimitiveType">Set</a> <a id="749" class="Symbol">(</a><a id="750" href="Data.Vec.Equality.html#539" class="Bound">s₁</a> <a id="753" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="755" href="Data.Vec.Equality.html#542" class="Bound">s₂</a><a id="757" class="Symbol">)</a> <a id="759" class="Keyword">where</a>
<a id="Equality._≈_.[]-cong" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a> <a id="778" class="Symbol">:</a> <a id="780" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="783" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="785" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>
<a id="Equality._≈_._∷-cong_" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">_∷-cong_</a> <a id="801" class="Symbol">:</a> <a id="803" class="Symbol">∀</a> <a id="805" class="Symbol">{</a><a id="806" href="Data.Vec.Equality.html#806" class="Bound">x¹</a> <a id="809" href="Data.Vec.Equality.html#809" class="Bound">n¹</a><a id="811" class="Symbol">}</a> <a id="813" class="Symbol">{</a><a id="814" href="Data.Vec.Equality.html#814" class="Bound">xs¹</a> <a id="818" class="Symbol">:</a> <a id="820" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="824" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="826" href="Data.Vec.Equality.html#809" class="Bound">n¹</a><a id="828" class="Symbol">}</a>
<a id="847" class="Symbol">{</a><a id="848" href="Data.Vec.Equality.html#848" class="Bound">x²</a> <a id="851" href="Data.Vec.Equality.html#851" class="Bound">n²</a><a id="853" class="Symbol">}</a> <a id="855" class="Symbol">{</a><a id="856" href="Data.Vec.Equality.html#856" class="Bound">xs²</a> <a id="860" class="Symbol">:</a> <a id="862" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="866" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="868" href="Data.Vec.Equality.html#851" class="Bound">n²</a><a id="870" class="Symbol">}</a>
<a id="889" class="Symbol">(</a><a id="890" href="Data.Vec.Equality.html#890" class="Bound">x¹≈x²</a> <a id="896" class="Symbol">:</a> <a id="898" href="Data.Vec.Equality.html#806" class="Bound">x¹</a> <a id="901" href="Relation.Binary.html#Equality.Equality.SS._%E2%89%8A_" class="Field Operator">≊</a> <a id="903" href="Data.Vec.Equality.html#848" class="Bound">x²</a><a id="905" class="Symbol">)</a> <a id="907" class="Symbol">(</a><a id="908" href="Data.Vec.Equality.html#908" class="Bound">xs¹≈xs²</a> <a id="916" class="Symbol">:</a> <a id="918" href="Data.Vec.Equality.html#814" class="Bound">xs¹</a> <a id="922" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="924" href="Data.Vec.Equality.html#856" class="Bound">xs²</a><a id="927" class="Symbol">)</a> <a id="929" class="Symbol">→</a>
<a id="948" href="Data.Vec.Equality.html#806" class="Bound">x¹</a> <a id="951" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="953" href="Data.Vec.Equality.html#814" class="Bound">xs¹</a> <a id="957" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="959" href="Data.Vec.Equality.html#848" class="Bound">x²</a> <a id="962" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="964" href="Data.Vec.Equality.html#856" class="Bound">xs²</a>
<a id="Equality.length-equal" href="Data.Vec.Equality.html#Equality.length-equal" class="Function">length-equal</a> <a id="984" class="Symbol">:</a> <a id="986" class="Symbol">∀</a> <a id="988" class="Symbol">{</a><a id="989" href="Data.Vec.Equality.html#989" class="Bound">n¹</a><a id="991" class="Symbol">}</a> <a id="993" class="Symbol">{</a><a id="994" href="Data.Vec.Equality.html#994" class="Bound">xs¹</a> <a id="998" class="Symbol">:</a> <a id="1000" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1004" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1006" href="Data.Vec.Equality.html#989" class="Bound">n¹</a><a id="1008" class="Symbol">}</a>
<a id="1029" class="Symbol">{</a><a id="1030" href="Data.Vec.Equality.html#1030" class="Bound">n²</a><a id="1032" class="Symbol">}</a> <a id="1034" class="Symbol">{</a><a id="1035" href="Data.Vec.Equality.html#1035" class="Bound">xs²</a> <a id="1039" class="Symbol">:</a> <a id="1041" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1045" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1047" href="Data.Vec.Equality.html#1030" class="Bound">n²</a><a id="1049" class="Symbol">}</a> <a id="1051" class="Symbol">→</a>
<a id="1070" href="Data.Vec.Equality.html#994" class="Bound">xs¹</a> <a id="1074" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1076" href="Data.Vec.Equality.html#1035" class="Bound">xs²</a> <a id="1080" class="Symbol">→</a> <a id="1082" href="Data.Vec.Equality.html#989" class="Bound">n¹</a> <a id="1085" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="1087" href="Data.Vec.Equality.html#1030" class="Bound">n²</a>
<a id="1092" href="Data.Vec.Equality.html#Equality.length-equal" class="Function">length-equal</a> <a id="1105" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a> <a id="1120" class="Symbol">=</a> <a id="1122" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>
<a id="1131" href="Data.Vec.Equality.html#Equality.length-equal" class="Function">length-equal</a> <a id="1144" class="Symbol">(_</a> <a id="1147" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1154" href="Data.Vec.Equality.html#1154" class="Bound">eq₂</a><a id="1157" class="Symbol">)</a> <a id="1159" class="Symbol">=</a> <a id="1161" href="Relation.Binary.PropositionalEquality.html#cong" class="Function">P.cong</a> <a id="1168" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1172" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1174" href="Data.Vec.Equality.html#Equality.length-equal" class="Function">length-equal</a> <a id="1187" href="Data.Vec.Equality.html#1154" class="Bound">eq₂</a>
<a id="Equality.refl" href="Data.Vec.Equality.html#Equality.refl" class="Function">refl</a> <a id="1199" class="Symbol">:</a> <a id="1201" class="Symbol">∀</a> <a id="1203" class="Symbol">{</a><a id="1204" href="Data.Vec.Equality.html#1204" class="Bound">n</a><a id="1205" class="Symbol">}</a> <a id="1207" class="Symbol">(</a><a id="1208" href="Data.Vec.Equality.html#1208" class="Bound">xs</a> <a id="1211" class="Symbol">:</a> <a id="1213" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1217" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1219" href="Data.Vec.Equality.html#1204" class="Bound">n</a><a id="1220" class="Symbol">)</a> <a id="1222" class="Symbol">→</a> <a id="1224" href="Data.Vec.Equality.html#1208" class="Bound">xs</a> <a id="1227" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1229" href="Data.Vec.Equality.html#1208" class="Bound">xs</a>
<a id="1234" href="Data.Vec.Equality.html#Equality.refl" class="Function">refl</a> <a id="1239" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="1248" class="Symbol">=</a> <a id="1250" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a>
<a id="1260" href="Data.Vec.Equality.html#Equality.refl" class="Function">refl</a> <a id="1265" class="Symbol">(</a><a id="1266" href="Data.Vec.Equality.html#1266" class="Bound">x</a> <a id="1268" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="1270" href="Data.Vec.Equality.html#1270" class="Bound">xs</a><a id="1272" class="Symbol">)</a> <a id="1274" class="Symbol">=</a> <a id="1276" href="Relation.Binary.Core.html#Equality.SS.refl" class="Function">SS.refl</a> <a id="1284" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1291" href="Data.Vec.Equality.html#Equality.refl" class="Function">refl</a> <a id="1296" href="Data.Vec.Equality.html#1270" class="Bound">xs</a>
<a id="Equality.sym" href="Data.Vec.Equality.html#Equality.sym" class="Function">sym</a> <a id="1306" class="Symbol">:</a> <a id="1308" class="Symbol">∀</a> <a id="1310" class="Symbol">{</a><a id="1311" href="Data.Vec.Equality.html#1311" class="Bound">n</a> <a id="1313" href="Data.Vec.Equality.html#1313" class="Bound">m</a><a id="1314" class="Symbol">}</a> <a id="1316" class="Symbol">{</a><a id="1317" href="Data.Vec.Equality.html#1317" class="Bound">xs</a> <a id="1320" class="Symbol">:</a> <a id="1322" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1326" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1328" href="Data.Vec.Equality.html#1311" class="Bound">n</a><a id="1329" class="Symbol">}</a> <a id="1331" class="Symbol">{</a><a id="1332" href="Data.Vec.Equality.html#1332" class="Bound">ys</a> <a id="1335" class="Symbol">:</a> <a id="1337" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1341" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1343" href="Data.Vec.Equality.html#1313" class="Bound">m</a><a id="1344" class="Symbol">}</a> <a id="1346" class="Symbol">→</a>
<a id="1356" href="Data.Vec.Equality.html#1317" class="Bound">xs</a> <a id="1359" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1361" href="Data.Vec.Equality.html#1332" class="Bound">ys</a> <a id="1364" class="Symbol">→</a> <a id="1366" href="Data.Vec.Equality.html#1332" class="Bound">ys</a> <a id="1369" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1371" href="Data.Vec.Equality.html#1317" class="Bound">xs</a>
<a id="1376" href="Data.Vec.Equality.html#Equality.sym" class="Function">sym</a> <a id="1380" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a> <a id="1403" class="Symbol">=</a> <a id="1405" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a>
<a id="1415" href="Data.Vec.Equality.html#Equality.sym" class="Function">sym</a> <a id="1419" class="Symbol">(</a><a id="1420" href="Data.Vec.Equality.html#1420" class="Bound">x¹≡x²</a> <a id="1426" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1433" href="Data.Vec.Equality.html#1433" class="Bound">xs¹≈xs²</a><a id="1440" class="Symbol">)</a> <a id="1442" class="Symbol">=</a> <a id="1444" href="Relation.Binary.Core.html#Equality.SS.sym" class="Function">SS.sym</a> <a id="1451" href="Data.Vec.Equality.html#1420" class="Bound">x¹≡x²</a> <a id="1457" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1464" href="Data.Vec.Equality.html#Equality.sym" class="Function">sym</a> <a id="1468" href="Data.Vec.Equality.html#1433" class="Bound">xs¹≈xs²</a>
<a id="Equality.trans" href="Data.Vec.Equality.html#Equality.trans" class="Function">trans</a> <a id="1485" class="Symbol">:</a> <a id="1487" class="Symbol">∀</a> <a id="1489" class="Symbol">{</a><a id="1490" href="Data.Vec.Equality.html#1490" class="Bound">n</a> <a id="1492" href="Data.Vec.Equality.html#1492" class="Bound">m</a> <a id="1494" href="Data.Vec.Equality.html#1494" class="Bound">l</a><a id="1495" class="Symbol">}</a> <a id="1497" class="Symbol">{</a><a id="1498" href="Data.Vec.Equality.html#1498" class="Bound">xs</a> <a id="1501" class="Symbol">:</a> <a id="1503" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1507" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1509" href="Data.Vec.Equality.html#1490" class="Bound">n</a><a id="1510" class="Symbol">}</a> <a id="1512" class="Symbol">{</a><a id="1513" href="Data.Vec.Equality.html#1513" class="Bound">ys</a> <a id="1516" class="Symbol">:</a> <a id="1518" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1522" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1524" href="Data.Vec.Equality.html#1492" class="Bound">m</a><a id="1525" class="Symbol">}</a> <a id="1527" class="Symbol">{</a><a id="1528" href="Data.Vec.Equality.html#1528" class="Bound">zs</a> <a id="1531" class="Symbol">:</a> <a id="1533" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1537" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1539" href="Data.Vec.Equality.html#1494" class="Bound">l</a><a id="1540" class="Symbol">}</a> <a id="1542" class="Symbol">→</a>
<a id="1554" href="Data.Vec.Equality.html#1498" class="Bound">xs</a> <a id="1557" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1559" href="Data.Vec.Equality.html#1513" class="Bound">ys</a> <a id="1562" class="Symbol">→</a> <a id="1564" href="Data.Vec.Equality.html#1513" class="Bound">ys</a> <a id="1567" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1569" href="Data.Vec.Equality.html#1528" class="Bound">zs</a> <a id="1572" class="Symbol">→</a> <a id="1574" href="Data.Vec.Equality.html#1498" class="Bound">xs</a> <a id="1577" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1579" href="Data.Vec.Equality.html#1528" class="Bound">zs</a>
<a id="1584" href="Data.Vec.Equality.html#Equality.trans" class="Function">trans</a> <a id="1590" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a> <a id="1609" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a> <a id="1628" class="Symbol">=</a> <a id="1630" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a>
<a id="1640" href="Data.Vec.Equality.html#Equality.trans" class="Function">trans</a> <a id="1646" class="Symbol">(</a><a id="1647" href="Data.Vec.Equality.html#1647" class="Bound">x≈y</a> <a id="1651" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1658" href="Data.Vec.Equality.html#1658" class="Bound">xs≈ys</a><a id="1663" class="Symbol">)</a> <a id="1665" class="Symbol">(</a><a id="1666" href="Data.Vec.Equality.html#1666" class="Bound">y≈z</a> <a id="1670" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1677" href="Data.Vec.Equality.html#1677" class="Bound">ys≈zs</a><a id="1682" class="Symbol">)</a> <a id="1684" class="Symbol">=</a>
<a id="1690" href="Relation.Binary.Core.html#Equality.SS.trans" class="Function">SS.trans</a> <a id="1699" href="Data.Vec.Equality.html#1647" class="Bound">x≈y</a> <a id="1703" href="Data.Vec.Equality.html#1666" class="Bound">y≈z</a> <a id="1707" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1714" href="Data.Vec.Equality.html#Equality.trans" class="Function">trans</a> <a id="1720" href="Data.Vec.Equality.html#1658" class="Bound">xs≈ys</a> <a id="1726" href="Data.Vec.Equality.html#1677" class="Bound">ys≈zs</a>
<a id="Equality.xs++[]≈xs" href="Data.Vec.Equality.html#Equality.xs%2B%2B%5B%5D%E2%89%88xs" class="Function">xs++[]≈xs</a> <a id="1745" class="Symbol">:</a> <a id="1747" class="Symbol">∀</a> <a id="1749" class="Symbol">{</a><a id="1750" href="Data.Vec.Equality.html#1750" class="Bound">n</a><a id="1751" class="Symbol">}</a> <a id="1753" class="Symbol">(</a><a id="1754" href="Data.Vec.Equality.html#1754" class="Bound">xs</a> <a id="1757" class="Symbol">:</a> <a id="1759" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1763" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1765" href="Data.Vec.Equality.html#1750" class="Bound">n</a><a id="1766" class="Symbol">)</a> <a id="1768" class="Symbol">→</a> <a id="1770" href="Data.Vec.Equality.html#1754" class="Bound">xs</a> <a id="1773" href="Data.Vec.html#_%2B%2B_" class="Function Operator">++</a> <a id="1776" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="1779" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="1781" href="Data.Vec.Equality.html#1754" class="Bound">xs</a>
<a id="1786" href="Data.Vec.Equality.html#Equality.xs%2B%2B%5B%5D%E2%89%88xs" class="Function">xs++[]≈xs</a> <a id="1796" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="1806" class="Symbol">=</a> <a id="1808" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a>
<a id="1818" href="Data.Vec.Equality.html#Equality.xs%2B%2B%5B%5D%E2%89%88xs" class="Function">xs++[]≈xs</a> <a id="1828" class="Symbol">(</a><a id="1829" href="Data.Vec.Equality.html#1829" class="Bound">x</a> <a id="1831" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="1833" href="Data.Vec.Equality.html#1833" class="Bound">xs</a><a id="1835" class="Symbol">)</a> <a id="1837" class="Symbol">=</a> <a id="1839" href="Relation.Binary.Core.html#Equality.SS.refl" class="Function">SS.refl</a> <a id="1847" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="1854" class="Symbol">(</a><a id="1855" href="Data.Vec.Equality.html#Equality.xs%2B%2B%5B%5D%E2%89%88xs" class="Function">xs++[]≈xs</a> <a id="1865" href="Data.Vec.Equality.html#1833" class="Bound">xs</a><a id="1867" class="Symbol">)</a>
<a id="Equality._++-cong_" href="Data.Vec.Equality.html#Equality._%2B%2B-cong_" class="Function Operator">_++-cong_</a> <a id="1882" class="Symbol">:</a> <a id="1884" class="Symbol">∀</a> <a id="1886" class="Symbol">{</a><a id="1887" href="Data.Vec.Equality.html#1887" class="Bound">n₁¹</a> <a id="1891" href="Data.Vec.Equality.html#1891" class="Bound">n₂¹</a><a id="1894" class="Symbol">}</a> <a id="1896" class="Symbol">{</a><a id="1897" href="Data.Vec.Equality.html#1897" class="Bound">xs₁¹</a> <a id="1902" class="Symbol">:</a> <a id="1904" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1908" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1910" href="Data.Vec.Equality.html#1887" class="Bound">n₁¹</a><a id="1913" class="Symbol">}</a> <a id="1915" class="Symbol">{</a><a id="1916" href="Data.Vec.Equality.html#1916" class="Bound">xs₂¹</a> <a id="1921" class="Symbol">:</a> <a id="1923" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1927" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1929" href="Data.Vec.Equality.html#1891" class="Bound">n₂¹</a><a id="1932" class="Symbol">}</a>
<a id="1950" class="Symbol">{</a><a id="1951" href="Data.Vec.Equality.html#1951" class="Bound">n₁²</a> <a id="1955" href="Data.Vec.Equality.html#1955" class="Bound">n₂²</a><a id="1958" class="Symbol">}</a> <a id="1960" class="Symbol">{</a><a id="1961" href="Data.Vec.Equality.html#1961" class="Bound">xs₁²</a> <a id="1966" class="Symbol">:</a> <a id="1968" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1972" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1974" href="Data.Vec.Equality.html#1951" class="Bound">n₁²</a><a id="1977" class="Symbol">}</a> <a id="1979" class="Symbol">{</a><a id="1980" href="Data.Vec.Equality.html#1980" class="Bound">xs₂²</a> <a id="1985" class="Symbol">:</a> <a id="1987" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1991" href="Relation.Binary.html#Equality.Equality.SS.A" class="Field">A</a> <a id="1993" href="Data.Vec.Equality.html#1955" class="Bound">n₂²</a><a id="1996" class="Symbol">}</a> <a id="1998" class="Symbol">→</a>
<a id="2014" href="Data.Vec.Equality.html#1897" class="Bound">xs₁¹</a> <a id="2019" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="2021" href="Data.Vec.Equality.html#1961" class="Bound">xs₁²</a> <a id="2026" class="Symbol">→</a> <a id="2028" href="Data.Vec.Equality.html#1916" class="Bound">xs₂¹</a> <a id="2033" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="2035" href="Data.Vec.Equality.html#1980" class="Bound">xs₂²</a> <a id="2040" class="Symbol">→</a>
<a id="2056" href="Data.Vec.Equality.html#1897" class="Bound">xs₁¹</a> <a id="2061" href="Data.Vec.html#_%2B%2B_" class="Function Operator">++</a> <a id="2064" href="Data.Vec.Equality.html#1916" class="Bound">xs₂¹</a> <a id="2069" href="Data.Vec.Equality.html#Equality._%E2%89%88_" class="Datatype Operator">≈</a> <a id="2071" href="Data.Vec.Equality.html#1961" class="Bound">xs₁²</a> <a id="2076" href="Data.Vec.html#_%2B%2B_" class="Function Operator">++</a> <a id="2079" href="Data.Vec.Equality.html#1980" class="Bound">xs₂²</a>
<a id="2086" href="Data.Vec.Equality.html#Equality._%E2%89%88_.%5B%5D-cong" class="InductiveConstructor">[]-cong</a> <a id="2103" href="Data.Vec.Equality.html#Equality._%2B%2B-cong_" class="Function Operator">++-cong</a> <a id="2111" href="Data.Vec.Equality.html#2111" class="Bound">eq₃</a> <a id="2115" class="Symbol">=</a> <a id="2117" href="Data.Vec.Equality.html#2111" class="Bound">eq₃</a>
<a id="2123" class="Symbol">(</a><a id="2124" href="Data.Vec.Equality.html#2124" class="Bound">eq₁</a> <a id="2128" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="2135" href="Data.Vec.Equality.html#2135" class="Bound">eq₂</a><a id="2138" class="Symbol">)</a> <a id="2140" href="Data.Vec.Equality.html#Equality._%2B%2B-cong_" class="Function Operator">++-cong</a> <a id="2148" href="Data.Vec.Equality.html#2148" class="Bound">eq₃</a> <a id="2152" class="Symbol">=</a> <a id="2154" href="Data.Vec.Equality.html#2124" class="Bound">eq₁</a> <a id="2158" href="Data.Vec.Equality.html#Equality._%E2%89%88_._%E2%88%B7-cong_" class="InductiveConstructor Operator">∷-cong</a> <a id="2165" class="Symbol">(</a><a id="2166" href="Data.Vec.Equality.html#2135" class="Bound">eq₂</a> <a id="2170" href="Data.Vec.Equality.html#Equality._%2B%2B-cong_" class="Function Operator">++-cong</a> <a id="2178" href="Data.Vec.Equality.html#2148" class="Bound">eq₃</a><a id="2181" class="Symbol">)</a>
<a id="2184" class="Keyword">module</a> <a id="DecidableEquality" href="Data.Vec.Equality.html#DecidableEquality" class="Module">DecidableEquality</a> <a id="2209" class="Symbol">{</a><a id="2210" href="Data.Vec.Equality.html#2210" class="Bound">d₁</a> <a id="2213" href="Data.Vec.Equality.html#2213" class="Bound">d₂</a><a id="2215" class="Symbol">}</a> <a id="2217" class="Symbol">(</a><a id="2218" href="Data.Vec.Equality.html#2218" class="Bound">D</a> <a id="2220" class="Symbol">:</a> <a id="2222" href="Relation.Binary.html#DecSetoid" class="Record">DecSetoid</a> <a id="2232" href="Data.Vec.Equality.html#2210" class="Bound">d₁</a> <a id="2235" href="Data.Vec.Equality.html#2213" class="Bound">d₂</a><a id="2237" class="Symbol">)</a> <a id="2239" class="Keyword">where</a>
<a id="2248" class="Keyword">private</a> <a id="2256" class="Keyword">module</a> <a id="DS" href="Data.Vec.Equality.html#DS" class="Module">DS</a> <a id="2266" class="Symbol">=</a> <a id="2268" href="Relation.Binary.html#DecSetoid" class="Module">DecSetoid</a> <a id="2278" href="Data.Vec.Equality.html#2218" class="Bound">D</a>
<a id="2282" class="Keyword">open</a> <a id="2287" href="Data.Vec.Equality.html#DS" class="Module">DS</a> <a id="2290" class="Keyword">using</a> <a id="2296" class="Symbol">()</a> <a id="2299" class="Keyword">renaming</a> <a id="2308" class="Symbol">(</a><a id="2309" href="Relation.Binary.html#Equality.DecidableEquality.DS._%E2%89%9F_" class="Function Operator">_≟_</a> <a id="2313" class="Symbol">to</a> <a id="2316" href="Relation.Binary.html#Equality.DecidableEquality.DS._%E2%89%9F_" class="Function Operator">_≟′_</a> <a id="2321" class="Symbol">;</a> <a id="2323" href="Relation.Binary.html#Equality.DecidableEquality.DS.Carrier" class="Field">Carrier</a> <a id="2331" class="Symbol">to</a> <a id="2334" href="Relation.Binary.html#Equality.DecidableEquality.DS.Carrier" class="Field">A</a><a id="2335" class="Symbol">)</a>
<a id="2339" class="Keyword">open</a> <a id="2344" href="Data.Vec.Equality.html#Equality" class="Module">Equality</a> <a id="2353" href="Relation.Binary.html#Equality.DecidableEquality.DS.setoid" class="Function">DS.setoid</a>
<a id="2365" class="Keyword">open</a> <a id="2370" class="Keyword">import</a> <a id="2377" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
<a id="2397" class="Keyword">infix</a> <a id="2403" class="Number">4</a> <a id="2405" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">_≟_</a>
<a id="DecidableEquality._≟_" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">_≟_</a> <a id="2416" class="Symbol">:</a> <a id="2418" class="Symbol">∀</a> <a id="2420" class="Symbol">{</a><a id="2421" href="Data.Vec.Equality.html#2421" class="Bound">n</a> <a id="2423" href="Data.Vec.Equality.html#2423" class="Bound">m</a><a id="2424" class="Symbol">}</a> <a id="2426" class="Symbol">(</a><a id="2427" href="Data.Vec.Equality.html#2427" class="Bound">xs</a> <a id="2430" class="Symbol">:</a> <a id="2432" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="2436" href="Relation.Binary.html#Equality.DecidableEquality.DS.A" class="Field">A</a> <a id="2438" href="Data.Vec.Equality.html#2421" class="Bound">n</a><a id="2439" class="Symbol">)</a> <a id="2441" class="Symbol">(</a><a id="2442" href="Data.Vec.Equality.html#2442" class="Bound">ys</a> <a id="2445" class="Symbol">:</a> <a id="2447" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="2451" href="Relation.Binary.html#Equality.DecidableEquality.DS.A" class="Field">A</a> <a id="2453" href="Data.Vec.Equality.html#2423" class="Bound">m</a><a id="2454" class="Symbol">)</a> <a id="2456" class="Symbol">→</a> <a id="2458" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="2462" class="Symbol">(</a><a id="2463" href="Data.Vec.Equality.html#2427" class="Bound">xs</a> <a id="2466" href="Data.Vec.Equality.html#686" class="Datatype Operator">≈</a> <a id="2468" href="Data.Vec.Equality.html#2442" class="Bound">ys</a><a id="2470" class="Symbol">)</a>
<a id="2474" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">_≟_</a> <a id="2478" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="2487" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="2496" class="Symbol">=</a> <a id="2498" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2502" href="Data.Vec.Equality.html#769" class="InductiveConstructor">[]-cong</a>
<a id="2512" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">_≟_</a> <a id="2516" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="2525" class="Symbol">(</a><a id="2526" href="Data.Vec.Equality.html#2526" class="Bound">y</a> <a id="2528" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2530" href="Data.Vec.Equality.html#2530" class="Bound">ys</a><a id="2532" class="Symbol">)</a> <a id="2534" class="Symbol">=</a> <a id="2536" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2539" class="Symbol">(λ())</a>
<a id="2547" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">_≟_</a> <a id="2551" class="Symbol">(</a><a id="2552" href="Data.Vec.Equality.html#2552" class="Bound">x</a> <a id="2554" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2556" href="Data.Vec.Equality.html#2556" class="Bound">xs</a><a id="2558" class="Symbol">)</a> <a id="2560" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="2569" class="Symbol">=</a> <a id="2571" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2574" class="Symbol">(λ())</a>
<a id="2582" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">_≟_</a> <a id="2586" class="Symbol">(</a><a id="2587" href="Data.Vec.Equality.html#2587" class="Bound">x</a> <a id="2589" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2591" href="Data.Vec.Equality.html#2591" class="Bound">xs</a><a id="2593" class="Symbol">)</a> <a id="2595" class="Symbol">(</a><a id="2596" href="Data.Vec.Equality.html#2596" class="Bound">y</a> <a id="2598" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2600" href="Data.Vec.Equality.html#2600" class="Bound">ys</a><a id="2602" class="Symbol">)</a> <a id="2604" class="Keyword">with</a> <a id="2609" href="Data.Vec.Equality.html#2591" class="Bound">xs</a> <a id="2612" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">≟</a> <a id="2614" href="Data.Vec.Equality.html#2600" class="Bound">ys</a> <a id="2617" class="Symbol">|</a> <a id="2619" href="Data.Vec.Equality.html#2587" class="Bound">x</a> <a id="2621" href="Relation.Binary.html#Equality.DecidableEquality.DS._%E2%89%9F%E2%80%B2_" class="Function Operator">≟′</a> <a id="2624" href="Data.Vec.Equality.html#2596" class="Bound">y</a>
<a id="2628" class="Symbol">...</a> <a id="2632" class="Symbol">|</a> <a id="2634" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2638" href="Data.Vec.Equality.html#2638" class="Bound">xs≈ys</a> <a id="2644" class="Symbol">|</a> <a id="2646" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2650" href="Data.Vec.Equality.html#2650" class="Bound">x≊y</a> <a id="2654" class="Symbol">=</a> <a id="2656" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2660" class="Symbol">(</a><a id="2661" href="Data.Vec.Equality.html#2650" class="Bound">x≊y</a> <a id="2665" href="Data.Vec.Equality.html#792" class="InductiveConstructor Operator">∷-cong</a> <a id="2672" href="Data.Vec.Equality.html#2638" class="Bound">xs≈ys</a><a id="2677" class="Symbol">)</a>
<a id="2681" class="Symbol">...</a> <a id="2685" class="Symbol">|</a> <a id="2687" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2690" href="Data.Vec.Equality.html#2690" class="Bound">¬xs≈ys</a> <a id="2697" class="Symbol">|</a> <a id="2699" class="Symbol">_</a> <a id="2707" class="Symbol">=</a> <a id="2709" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2712" href="Data.Vec.Equality.html#2733" class="Function">helper</a>
<a id="2723" class="Keyword">where</a>
<a id="2733" href="Data.Vec.Equality.html#2733" class="Function">helper</a> <a id="2740" class="Symbol">:</a> <a id="2742" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="2744" class="Symbol">(</a><a id="2745" class="Bound">x</a> <a id="2747" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2749" class="Bound">xs</a> <a id="2752" href="Data.Vec.Equality.html#686" class="Datatype Operator">≈</a> <a id="2754" class="Bound">y</a> <a id="2756" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2758" class="Bound">ys</a><a id="2760" class="Symbol">)</a>
<a id="2766" href="Data.Vec.Equality.html#2733" class="Function">helper</a> <a id="2773" class="Symbol">(_</a> <a id="2776" href="Data.Vec.Equality.html#792" class="InductiveConstructor Operator">∷-cong</a> <a id="2783" href="Data.Vec.Equality.html#2783" class="Bound">xs≈ys</a><a id="2788" class="Symbol">)</a> <a id="2790" class="Symbol">=</a> <a id="2792" href="Data.Vec.Equality.html#2690" class="Bound">¬xs≈ys</a> <a id="2799" href="Data.Vec.Equality.html#2783" class="Bound">xs≈ys</a>
<a id="2807" class="CatchallClause Symbol">...</a><a id="2810" class="CatchallClause"> </a><a id="2811" class="CatchallClause Symbol">|</a><a id="2812" class="CatchallClause"> </a><a id="2813" class="CatchallClause Symbol">_</a><a id="2814" class="CatchallClause"> </a><a id="2823" class="CatchallClause Symbol">|</a><a id="2824" class="CatchallClause"> </a><a id="2825" href="Relation.Nullary.html#Dec.no" class="CatchallClause InductiveConstructor">no</a><a id="2827" class="CatchallClause"> </a><a id="2828" href="Data.Vec.Equality.html#2828" class="CatchallClause Bound">¬x≊y</a> <a id="2833" class="Symbol">=</a> <a id="2835" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2838" href="Data.Vec.Equality.html#2859" class="Function">helper</a>
<a id="2849" class="Keyword">where</a>
<a id="2859" href="Data.Vec.Equality.html#2859" class="Function">helper</a> <a id="2866" class="Symbol">:</a> <a id="2868" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="2870" class="Symbol">(</a><a id="2871" class="Bound">x</a> <a id="2873" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2875" class="Bound">xs</a> <a id="2878" href="Data.Vec.Equality.html#686" class="Datatype Operator">≈</a> <a id="2880" class="Bound">y</a> <a id="2882" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2884" class="Bound">ys</a><a id="2886" class="Symbol">)</a>
<a id="2892" href="Data.Vec.Equality.html#2859" class="Function">helper</a> <a id="2899" class="Symbol">(</a><a id="2900" href="Data.Vec.Equality.html#2900" class="Bound">x≊y</a> <a id="2904" href="Data.Vec.Equality.html#792" class="InductiveConstructor Operator">∷-cong</a> <a id="2911" class="Symbol">_)</a> <a id="2914" class="Symbol">=</a> <a id="2916" href="Data.Vec.Equality.html#2828" class="Bound">¬x≊y</a> <a id="2921" href="Data.Vec.Equality.html#2900" class="Bound">x≊y</a>
<a id="2926" class="Keyword">module</a> <a id="PropositionalEquality" href="Data.Vec.Equality.html#PropositionalEquality" class="Module">PropositionalEquality</a> <a id="2955" class="Symbol">{</a><a id="2956" href="Data.Vec.Equality.html#2956" class="Bound">a</a><a id="2957" class="Symbol">}</a> <a id="2959" class="Symbol">{</a><a id="2960" href="Data.Vec.Equality.html#2960" class="Bound">A</a> <a id="2962" class="Symbol">:</a> <a id="2964" class="PrimitiveType">Set</a> <a id="2968" href="Data.Vec.Equality.html#2956" class="Bound">a</a><a id="2969" class="Symbol">}</a> <a id="2971" class="Keyword">where</a>
<a id="2980" class="Keyword">open</a> <a id="2985" href="Data.Vec.Equality.html#Equality" class="Module">Equality</a> <a id="2994" class="Symbol">(</a><a id="2995" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="3004" href="Data.Vec.Equality.html#2960" class="Bound">A</a><a id="3005" class="Symbol">)</a> <a id="3007" class="Keyword">public</a>
<a id="PropositionalEquality.to-≡" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%A1" class="Function">to-≡</a> <a id="3022" class="Symbol">:</a> <a id="3024" class="Symbol">∀</a> <a id="3026" class="Symbol">{</a><a id="3027" href="Data.Vec.Equality.html#3027" class="Bound">n</a><a id="3028" class="Symbol">}</a> <a id="3030" class="Symbol">{</a><a id="3031" href="Data.Vec.Equality.html#3031" class="Bound">xs</a> <a id="3034" href="Data.Vec.Equality.html#3034" class="Bound">ys</a> <a id="3037" class="Symbol">:</a> <a id="3039" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="3043" href="Data.Vec.Equality.html#2960" class="Bound">A</a> <a id="3045" href="Data.Vec.Equality.html#3027" class="Bound">n</a><a id="3046" class="Symbol">}</a> <a id="3048" class="Symbol">→</a> <a id="3050" href="Data.Vec.Equality.html#3031" class="Bound">xs</a> <a id="3053" href="Data.Vec.Equality.html#686" class="Datatype Operator">≈</a> <a id="3055" href="Data.Vec.Equality.html#3034" class="Bound">ys</a> <a id="3058" class="Symbol">→</a> <a id="3060" href="Data.Vec.Equality.html#3031" class="Bound">xs</a> <a id="3063" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="3065" href="Data.Vec.Equality.html#3034" class="Bound">ys</a>
<a id="3070" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%A1" class="Function">to-≡</a> <a id="3075" href="Data.Vec.Equality.html#769" class="InductiveConstructor">[]-cong</a> <a id="3099" class="Symbol">=</a> <a id="3101" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a>
<a id="3110" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%A1" class="Function">to-≡</a> <a id="3115" class="Symbol">(</a><a id="3116" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="3123" href="Data.Vec.Equality.html#792" class="InductiveConstructor Operator">∷-cong</a> <a id="3130" href="Data.Vec.Equality.html#3130" class="Bound">xs¹≈xs²</a><a id="3137" class="Symbol">)</a> <a id="3139" class="Symbol">=</a> <a id="3141" href="Relation.Binary.PropositionalEquality.html#cong" class="Function">P.cong</a> <a id="3148" class="Symbol">(</a><a id="3149" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">_∷_</a> <a id="3153" class="Symbol">_)</a> <a id="3156" href="Function.html#_%24_" class="Function Operator">$</a> <a id="3158" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%A1" class="Function">to-≡</a> <a id="3163" href="Data.Vec.Equality.html#3130" class="Bound">xs¹≈xs²</a>
<a id="PropositionalEquality.from-≡" href="Data.Vec.Equality.html#PropositionalEquality.from-%E2%89%A1" class="Function">from-≡</a> <a id="3181" class="Symbol">:</a> <a id="3183" class="Symbol">∀</a> <a id="3185" class="Symbol">{</a><a id="3186" href="Data.Vec.Equality.html#3186" class="Bound">n</a><a id="3187" class="Symbol">}</a> <a id="3189" class="Symbol">{</a><a id="3190" href="Data.Vec.Equality.html#3190" class="Bound">xs</a> <a id="3193" href="Data.Vec.Equality.html#3193" class="Bound">ys</a> <a id="3196" class="Symbol">:</a> <a id="3198" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="3202" href="Data.Vec.Equality.html#2960" class="Bound">A</a> <a id="3204" href="Data.Vec.Equality.html#3186" class="Bound">n</a><a id="3205" class="Symbol">}</a> <a id="3207" class="Symbol">→</a> <a id="3209" href="Data.Vec.Equality.html#3190" class="Bound">xs</a> <a id="3212" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="3214" href="Data.Vec.Equality.html#3193" class="Bound">ys</a> <a id="3217" class="Symbol">→</a> <a id="3219" href="Data.Vec.Equality.html#3190" class="Bound">xs</a> <a id="3222" href="Data.Vec.Equality.html#686" class="Datatype Operator">≈</a> <a id="3224" href="Data.Vec.Equality.html#3193" class="Bound">ys</a>
<a id="3229" href="Data.Vec.Equality.html#PropositionalEquality.from-%E2%89%A1" class="Function">from-≡</a> <a id="3236" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="3243" class="Symbol">=</a> <a id="3245" href="Data.Vec.Equality.html#1194" class="Function">refl</a> <a id="3250" class="Symbol">_</a>
<a id="PropositionalEquality.to-≅" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%85" class="Function">to-≅</a> <a id="3260" class="Symbol">:</a> <a id="3262" class="Symbol">∀</a> <a id="3264" class="Symbol">{</a><a id="3265" href="Data.Vec.Equality.html#3265" class="Bound">m</a> <a id="3267" href="Data.Vec.Equality.html#3267" class="Bound">n</a><a id="3268" class="Symbol">}</a> <a id="3270" class="Symbol">{</a><a id="3271" href="Data.Vec.Equality.html#3271" class="Bound">xs</a> <a id="3274" class="Symbol">:</a> <a id="3276" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="3280" href="Data.Vec.Equality.html#2960" class="Bound">A</a> <a id="3282" href="Data.Vec.Equality.html#3265" class="Bound">m</a><a id="3283" class="Symbol">}</a> <a id="3285" class="Symbol">{</a><a id="3286" href="Data.Vec.Equality.html#3286" class="Bound">ys</a> <a id="3289" class="Symbol">:</a> <a id="3291" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="3295" href="Data.Vec.Equality.html#2960" class="Bound">A</a> <a id="3297" href="Data.Vec.Equality.html#3267" class="Bound">n</a><a id="3298" class="Symbol">}</a> <a id="3300" class="Symbol">→</a>
<a id="3314" href="Data.Vec.Equality.html#3271" class="Bound">xs</a> <a id="3317" href="Data.Vec.Equality.html#686" class="Datatype Operator">≈</a> <a id="3319" href="Data.Vec.Equality.html#3286" class="Bound">ys</a> <a id="3322" class="Symbol">→</a> <a id="3324" href="Data.Vec.Equality.html#3271" class="Bound">xs</a> <a id="3327" href="Relation.Binary.HeterogeneousEquality.Core.html#_%E2%89%85_" class="Datatype Operator">≅</a> <a id="3329" href="Data.Vec.Equality.html#3286" class="Bound">ys</a>
<a id="3334" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%85" class="Function">to-≅</a> <a id="3339" href="Data.Vec.Equality.html#3339" class="Bound">p</a> <a id="3341" class="Keyword">with</a> <a id="3346" href="Data.Vec.Equality.html#971" class="Function">length-equal</a> <a id="3359" href="Data.Vec.Equality.html#3339" class="Bound">p</a>
<a id="3363" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%85" class="Function">to-≅</a> <a id="3368" href="Data.Vec.Equality.html#3368" class="Bound">p</a> <a id="3370" class="Symbol">|</a> <a id="3372" href="Agda.Builtin.Equality.html#_%E2%89%A1_.refl" class="InductiveConstructor">P.refl</a> <a id="3379" class="Symbol">=</a> <a id="3381" href="Relation.Binary.HeterogeneousEquality.html#%E2%89%A1-to-%E2%89%85" class="Function">H.≡-to-≅</a> <a id="3390" class="Symbol">(</a><a id="3391" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%A1" class="Function">to-≡</a> <a id="3396" href="Data.Vec.Equality.html#3368" class="Bound">p</a><a id="3397" class="Symbol">)</a>
<a id="PropositionalEquality.xs++[]≅xs" href="Data.Vec.Equality.html#PropositionalEquality.xs%2B%2B%5B%5D%E2%89%85xs" class="Function">xs++[]≅xs</a> <a id="3412" class="Symbol">:</a> <a id="3414" class="Symbol">∀</a> <a id="3416" class="Symbol">{</a><a id="3417" href="Data.Vec.Equality.html#3417" class="Bound">n</a><a id="3418" class="Symbol">}</a> <a id="3420" class="Symbol">→</a> <a id="3422" class="Symbol">(</a><a id="3423" href="Data.Vec.Equality.html#3423" class="Bound">xs</a> <a id="3426" class="Symbol">:</a> <a id="3428" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="3432" href="Data.Vec.Equality.html#2960" class="Bound">A</a> <a id="3434" href="Data.Vec.Equality.html#3417" class="Bound">n</a><a id="3435" class="Symbol">)</a> <a id="3437" class="Symbol">→</a> <a id="3439" class="Symbol">(</a><a id="3440" href="Data.Vec.Equality.html#3423" class="Bound">xs</a> <a id="3443" href="Data.Vec.html#_%2B%2B_" class="Function Operator">++</a> <a id="3446" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a><a id="3448" class="Symbol">)</a> <a id="3450" href="Relation.Binary.HeterogeneousEquality.Core.html#_%E2%89%85_" class="Datatype Operator">≅</a> <a id="3452" href="Data.Vec.Equality.html#3423" class="Bound">xs</a>
<a id="3457" href="Data.Vec.Equality.html#PropositionalEquality.xs%2B%2B%5B%5D%E2%89%85xs" class="Function">xs++[]≅xs</a> <a id="3467" href="Data.Vec.Equality.html#3467" class="Bound">xs</a> <a id="3470" class="Symbol">=</a> <a id="3472" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%85" class="Function">to-≅</a> <a id="3477" class="Symbol">(</a><a id="3478" href="Data.Vec.Equality.html#1735" class="Function">xs++[]≈xs</a> <a id="3488" href="Data.Vec.Equality.html#3467" class="Bound">xs</a><a id="3490" class="Symbol">)</a>
</pre></body></html>
|