Deploying to gh-pages from @ 4a8cd32 🚀

master/Data.List.Relation.Binary.Sublist.DecSetoid.html

@@ -37,7 +37,7 @@
 <a id="1224" class="Comment">-- Additional relational properties</a>
 
 <a id="_⊆?_"></a><a id="1261" href="Data.List.Relation.Binary.Sublist.DecSetoid.html#1261" class="Function Operator">_⊆?_</a> <a id="1266" class="Symbol">:</a> <a id="1268" href="Relation.Binary.Definitions.html#6713" class="Function">Decidable</a> <a id="1278" href="Data.List.Relation.Binary.Sublist.Setoid.html#1567" class="Function Operator">_⊆_</a>
-<a id="1282" href="Data.List.Relation.Binary.Sublist.DecSetoid.html#1261" class="Function Operator">_⊆?_</a> <a id="1287" class="Symbol">=</a> <a id="1289" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#15799" class="Function">HeterogeneousProperties.sublist?</a> <a id="1322" href="Relation.Binary.Structures.html#1949" class="Function Operator">_≟_</a>
+<a id="1282" href="Data.List.Relation.Binary.Sublist.DecSetoid.html#1261" class="Function Operator">_⊆?_</a> <a id="1287" class="Symbol">=</a> <a id="1289" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#15901" class="Function">HeterogeneousProperties.sublist?</a> <a id="1322" href="Relation.Binary.Structures.html#1949" class="Function Operator">_≟_</a>
 
 <a id="⊆-isDecPartialOrder"></a><a id="1327" href="Data.List.Relation.Binary.Sublist.DecSetoid.html#1327" class="Function">⊆-isDecPartialOrder</a> <a id="1347" class="Symbol">:</a> <a id="1349" href="Relation.Binary.Structures.html#4251" class="Record">IsDecPartialOrder</a> <a id="1367" href="Data.List.Relation.Binary.Equality.Setoid.html#1555" class="Function Operator">_≋_</a> <a id="1371" href="Data.List.Relation.Binary.Sublist.Setoid.html#1567" class="Function Operator">_⊆_</a>
 <a id="1375" href="Data.List.Relation.Binary.Sublist.DecSetoid.html#1327" class="Function">⊆-isDecPartialOrder</a> <a id="1395" class="Symbol">=</a> <a id="1397" class="Keyword">record</a>

master/Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html

@@ -118,11 +118,11 @@
 <a id="3808" class="Keyword">private</a>
 
   <a id="keep-it"></a><a id="3819" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3819" class="Function">keep-it</a> <a id="3827" class="Symbol">:</a> <a id="3829" class="Symbol">∀</a> <a id="3831" class="Symbol">{</a><a id="3832" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3832" class="Bound">n</a> <a id="3834" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3834" class="Bound">a</a> <a id="3836" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3836" class="Bound">b</a><a id="3837" class="Symbol">}</a> <a id="3839" class="Symbol">→</a> <a id="3841" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3834" class="Bound">a</a> <a id="3843" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2524" class="Datatype Operator">⊆I</a> <a id="3846" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3836" class="Bound">b</a> <a id="3848" class="Symbol">→</a> <a id="3850" class="Symbol">(</a><a id="3851" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3851" class="Bound">xs</a> <a id="3854" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3854" class="Bound">ys</a> <a id="3857" class="Symbol">:</a> <a id="3859" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2116" class="Function">RList</a> <a id="3865" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3832" class="Bound">n</a><a id="3866" class="Symbol">)</a> <a id="3868" class="Symbol">→</a> <a id="3870" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3851" class="Bound">xs</a> <a id="3873" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2746" class="Function Operator">⊆R</a> <a id="3876" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3854" class="Bound">ys</a> <a id="3879" class="Symbol">→</a> <a id="3881" class="Symbol">(</a><a id="3882" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3834" class="Bound">a</a> <a id="3884" class="InductiveConstructor Operator">∷</a> <a id="3886" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3851" class="Bound">xs</a><a id="3888" class="Symbol">)</a> <a id="3890" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2746" class="Function Operator">⊆R</a> <a id="3893" class="Symbol">(</a><a id="3894" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3836" class="Bound">b</a> <a id="3896" class="InductiveConstructor Operator">∷</a> <a id="3898" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3854" class="Bound">ys</a><a id="3900" class="Symbol">)</a>
-  <a id="3904" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3819" class="Function">keep-it</a> <a id="3912" class="Symbol">(</a><a id="3913" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2572" class="InductiveConstructor">var</a> <a id="3917" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3917" class="Bound">a≡b</a><a id="3920" class="Symbol">)</a> <a id="3922" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3922" class="Bound">xs</a> <a id="3925" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3925" class="Bound">ys</a> <a id="3928" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3928" class="Bound">hyp</a> <a id="3932" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3932" class="Bound">ρ</a> <a id="3934" class="Symbol">=</a> <a id="3936" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#7199" class="Function">++⁺</a> <a id="3940" class="Symbol">(</a><a id="3941" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#14194" class="Function">reflexive</a> <a id="3951" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#504" class="Bound">R-refl</a> <a id="3958" class="Symbol">(</a><a id="3959" href="Relation.Binary.PropositionalEquality.Core.html#1339" class="Function">cong</a> <a id="3964" class="Symbol">_</a> <a id="3966" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3917" class="Bound">a≡b</a><a id="3969" class="Symbol">))</a> <a id="3972" class="Symbol">(</a><a id="3973" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3928" class="Bound">hyp</a> <a id="3977" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3932" class="Bound">ρ</a><a id="3978" class="Symbol">)</a>
+  <a id="3904" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3819" class="Function">keep-it</a> <a id="3912" class="Symbol">(</a><a id="3913" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2572" class="InductiveConstructor">var</a> <a id="3917" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3917" class="Bound">a≡b</a><a id="3920" class="Symbol">)</a> <a id="3922" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3922" class="Bound">xs</a> <a id="3925" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3925" class="Bound">ys</a> <a id="3928" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3928" class="Bound">hyp</a> <a id="3932" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3932" class="Bound">ρ</a> <a id="3934" class="Symbol">=</a> <a id="3936" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#7301" class="Function">++⁺</a> <a id="3940" class="Symbol">(</a><a id="3941" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#14296" class="Function">reflexive</a> <a id="3951" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#504" class="Bound">R-refl</a> <a id="3958" class="Symbol">(</a><a id="3959" href="Relation.Binary.PropositionalEquality.Core.html#1339" class="Function">cong</a> <a id="3964" class="Symbol">_</a> <a id="3966" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3917" class="Bound">a≡b</a><a id="3969" class="Symbol">))</a> <a id="3972" class="Symbol">(</a><a id="3973" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3928" class="Bound">hyp</a> <a id="3977" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3932" class="Bound">ρ</a><a id="3978" class="Symbol">)</a>
   <a id="3982" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3819" class="Function">keep-it</a> <a id="3990" class="Symbol">(</a><a id="3991" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2613" class="InductiveConstructor">val</a> <a id="3995" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3995" class="Bound">rab</a><a id="3998" class="Symbol">)</a> <a id="4000" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4000" class="Bound">xs</a> <a id="4003" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4003" class="Bound">ys</a> <a id="4006" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4006" class="Bound">hyp</a> <a id="4010" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4010" class="Bound">ρ</a> <a id="4012" class="Symbol">=</a> <a id="4014" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#3995" class="Bound">rab</a> <a id="4018" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Core.html#1024" class="InductiveConstructor Operator">∷</a> <a id="4020" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4006" class="Bound">hyp</a> <a id="4024" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4010" class="Bound">ρ</a>
 
   <a id="skip-it"></a><a id="4029" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4029" class="Function">skip-it</a> <a id="4037" class="Symbol">:</a> <a id="4039" class="Symbol">∀</a> <a id="4041" class="Symbol">{</a><a id="4042" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4042" class="Bound">n</a><a id="4043" class="Symbol">}</a> <a id="4045" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4045" class="Bound">it</a> <a id="4048" class="Symbol">(</a><a id="4049" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4049" class="Bound">d</a> <a id="4051" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4051" class="Bound">e</a> <a id="4053" class="Symbol">:</a> <a id="4055" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2116" class="Function">RList</a> <a id="4061" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4042" class="Bound">n</a><a id="4062" class="Symbol">)</a> <a id="4064" class="Symbol">→</a> <a id="4066" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4049" class="Bound">d</a> <a id="4068" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2746" class="Function Operator">⊆R</a> <a id="4071" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4051" class="Bound">e</a> <a id="4073" class="Symbol">→</a> <a id="4075" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4049" class="Bound">d</a> <a id="4077" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2746" class="Function Operator">⊆R</a> <a id="4080" class="Symbol">(</a><a id="4081" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4045" class="Bound">it</a> <a id="4084" class="InductiveConstructor Operator">∷</a> <a id="4086" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4051" class="Bound">e</a><a id="4087" class="Symbol">)</a>
-  <a id="4091" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4029" class="Function">skip-it</a> <a id="4099" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4099" class="Bound">it</a> <a id="4102" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4102" class="Bound">d</a> <a id="4104" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4104" class="Bound">ys</a> <a id="4107" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4107" class="Bound">hyp</a> <a id="4111" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4111" class="Bound">ρ</a> <a id="4113" class="Symbol">=</a> <a id="4115" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#7592" class="Function">++ˡ</a> <a id="4119" class="Symbol">(</a><a id="4120" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2174" class="Function Operator">⟦</a> <a id="4122" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4099" class="Bound">it</a> <a id="4125" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2174" class="Function Operator">⟧I</a> <a id="4128" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4111" class="Bound">ρ</a><a id="4129" class="Symbol">)</a> <a id="4131" class="Symbol">(</a><a id="4132" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4107" class="Bound">hyp</a> <a id="4136" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4111" class="Bound">ρ</a><a id="4137" class="Symbol">)</a>
+  <a id="4091" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4029" class="Function">skip-it</a> <a id="4099" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4099" class="Bound">it</a> <a id="4102" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4102" class="Bound">d</a> <a id="4104" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4104" class="Bound">ys</a> <a id="4107" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4107" class="Bound">hyp</a> <a id="4111" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4111" class="Bound">ρ</a> <a id="4113" class="Symbol">=</a> <a id="4115" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Properties.html#7694" class="Function">++ˡ</a> <a id="4119" class="Symbol">(</a><a id="4120" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2174" class="Function Operator">⟦</a> <a id="4122" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4099" class="Bound">it</a> <a id="4125" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2174" class="Function Operator">⟧I</a> <a id="4128" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4111" class="Bound">ρ</a><a id="4129" class="Symbol">)</a> <a id="4131" class="Symbol">(</a><a id="4132" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4107" class="Bound">hyp</a> <a id="4136" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4111" class="Bound">ρ</a><a id="4137" class="Symbol">)</a>
 
 <a id="4140" class="Comment">-- Solver for items</a>
 <a id="solveI"></a><a id="4160" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4160" class="Function">solveI</a> <a id="4167" class="Symbol">:</a> <a id="4169" class="Symbol">∀</a> <a id="4171" class="Symbol">{</a><a id="4172" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4172" class="Bound">n</a><a id="4173" class="Symbol">}</a> <a id="4175" class="Symbol">(</a><a id="4176" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4176" class="Bound">a</a> <a id="4178" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4178" class="Bound">b</a> <a id="4180" class="Symbol">:</a> <a id="4182" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#1853" class="Datatype">Item</a> <a id="4187" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4172" class="Bound">n</a><a id="4188" class="Symbol">)</a> <a id="4190" class="Symbol">→</a> <a id="4192" href="Agda.Builtin.Maybe.html#135" class="Datatype">Maybe</a> <a id="4198" class="Symbol">(</a><a id="4199" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4176" class="Bound">a</a> <a id="4201" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#2524" class="Datatype Operator">⊆I</a> <a id="4204" href="Data.List.Relation.Binary.Sublist.Heterogeneous.Solver.html#4178" class="Bound">b</a><a id="4205" class="Symbol">)</a>