Skip to content

Commit

Permalink
Deploying to gh-pages from @ 279fa18 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Jan 3, 2025
1 parent 6c35abc commit 70e1607
Show file tree
Hide file tree
Showing 8 changed files with 1,529 additions and 1,534 deletions.
4 changes: 2 additions & 2 deletions master/Algebra.Lattice.Properties.BooleanAlgebra.Expression.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
<a id="608" class="Keyword">open</a> <a id="613" class="Keyword">import</a> <a id="620" href="Data.Vec.Base.html" class="Module">Data.Vec.Base</a> <a id="634" class="Symbol">as</a> <a id="637" class="Module">Vec</a> <a id="641" class="Keyword">using</a> <a id="647" class="Symbol">(</a><a id="648" href="Data.Vec.Base.html#1119" class="Datatype">Vec</a><a id="651" class="Symbol">)</a>
<a id="653" class="Keyword">import</a> <a id="660" href="Data.Vec.Effectful.html" class="Module">Data.Vec.Effectful</a> <a id="679" class="Symbol">as</a> <a id="682" class="Module">Vec</a>
<a id="686" class="Keyword">import</a> <a id="693" href="Function.Identity.Effectful.html" class="Module">Function.Identity.Effectful</a> <a id="721" class="Symbol">as</a> <a id="724" class="Module">Identity</a>
<a id="733" class="Keyword">open</a> <a id="738" class="Keyword">import</a> <a id="745" href="Data.Vec.Properties.html" class="Module">Data.Vec.Properties</a> <a id="765" class="Keyword">using</a> <a id="771" class="Symbol">(</a><a id="772" href="Data.Vec.Properties.html#16840" class="Function">lookup-map</a><a id="782" class="Symbol">)</a>
<a id="733" class="Keyword">open</a> <a id="738" class="Keyword">import</a> <a id="745" href="Data.Vec.Properties.html" class="Module">Data.Vec.Properties</a> <a id="765" class="Keyword">using</a> <a id="771" class="Symbol">(</a><a id="772" href="Data.Vec.Properties.html#16784" class="Function">lookup-map</a><a id="782" class="Symbol">)</a>
<a id="784" class="Keyword">open</a> <a id="789" class="Keyword">import</a> <a id="796" href="Data.Vec.Relation.Binary.Pointwise.Extensional.html" class="Module">Data.Vec.Relation.Binary.Pointwise.Extensional</a> <a id="843" class="Symbol">as</a> <a id="846" class="Module">PW</a>
<a id="851" class="Keyword">using</a> <a id="857" class="Symbol">(</a><a id="858" href="Data.Vec.Relation.Binary.Pointwise.Extensional.html#1498" class="Record">Pointwise</a><a id="867" class="Symbol">;</a> <a id="869" href="Data.Vec.Relation.Binary.Pointwise.Extensional.html#1664" class="InductiveConstructor">ext</a><a id="872" class="Symbol">)</a>
<a id="874" class="Keyword">open</a> <a id="879" class="Keyword">import</a> <a id="886" href="Effect.Applicative.html" class="Module">Effect.Applicative</a> <a id="905" class="Symbol">as</a> <a id="908" class="Module">Applicative</a>
Expand Down Expand Up @@ -80,7 +80,7 @@

<a id="Naturality.natural"></a><a id="2384" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2384" class="Function">natural</a> <a id="2392" class="Symbol">:</a> <a id="2394" class="Symbol">∀</a> <a id="2396" class="Symbol">{</a><a id="2397" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2397" class="Bound">n</a><a id="2398" class="Symbol">}</a> <a id="2400" class="Symbol">(</a><a id="2401" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2401" class="Bound">e</a> <a id="2403" class="Symbol">:</a> <a id="2405" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1296" class="Datatype">Expr</a> <a id="2410" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2397" class="Bound">n</a><a id="2411" class="Symbol">)</a> <a id="2413" class="Symbol">→</a> <a id="2415" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2418" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="2420" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2172" class="Function Operator">⟦</a> <a id="2422" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2401" class="Bound">e</a> <a id="2424" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2172" class="Function Operator">⟧₁</a> <a id="2427" href="Relation.Binary.PropositionalEquality.Core.html#1012" class="Function Operator">≗</a> <a id="2429" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2215" class="Function Operator">⟦</a> <a id="2431" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2401" class="Bound">e</a> <a id="2433" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2215" class="Function Operator">⟧₂</a> <a id="2436" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="2438" href="Data.Vec.Base.html#2955" class="Function">Vec.map</a> <a id="2446" href="Effect.Functor.html#1149" class="Function">op</a>
<a id="2451" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2384" class="Function">natural</a> <a id="2459" class="Symbol">(</a><a id="2460" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1319" class="InductiveConstructor">var</a> <a id="2464" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2464" class="Bound">x</a><a id="2465" class="Symbol">)</a> <a id="2467" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2467" class="Bound">ρ</a> <a id="2469" class="Symbol">=</a> <a id="2471" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
<a id="2481" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2484" class="Symbol">(</a><a id="2485" href="Data.Vec.Base.html#1676" class="Function">Vec.lookup</a> <a id="2496" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2467" class="Bound">ρ</a> <a id="2498" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2464" class="Bound">x</a><a id="2499" class="Symbol">)</a> <a id="2544" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2547" href="Relation.Binary.PropositionalEquality.Core.html#1893" class="Function">≡.sym</a> <a id="2553" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="2555" href="Data.Vec.Properties.html#16840" class="Function">lookup-map</a> <a id="2566" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2464" class="Bound">x</a> <a id="2568" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2571" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2467" class="Bound">ρ</a> <a id="2573" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
<a id="2481" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2484" class="Symbol">(</a><a id="2485" href="Data.Vec.Base.html#1676" class="Function">Vec.lookup</a> <a id="2496" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2467" class="Bound">ρ</a> <a id="2498" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2464" class="Bound">x</a><a id="2499" class="Symbol">)</a> <a id="2544" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2547" href="Relation.Binary.PropositionalEquality.Core.html#1893" class="Function">≡.sym</a> <a id="2553" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="2555" href="Data.Vec.Properties.html#16784" class="Function">lookup-map</a> <a id="2566" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2464" class="Bound">x</a> <a id="2568" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2571" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2467" class="Bound">ρ</a> <a id="2573" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
<a id="2579" href="Data.Vec.Base.html#1676" class="Function">Vec.lookup</a> <a id="2590" class="Symbol">(</a><a id="2591" href="Data.Vec.Base.html#2955" class="Function">Vec.map</a> <a id="2599" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2602" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2467" class="Bound">ρ</a><a id="2603" class="Symbol">)</a> <a id="2605" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2464" class="Bound">x</a> <a id="2642" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
<a id="2646" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2384" class="Function">natural</a> <a id="2654" class="Symbol">(</a><a id="2655" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2655" class="Bound">e₁</a> <a id="2658" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#1355" class="InductiveConstructor Operator">or</a> <a id="2661" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2661" class="Bound">e₂</a><a id="2663" class="Symbol">)</a> <a id="2665" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2665" class="Bound">ρ</a> <a id="2667" class="Symbol">=</a> <a id="2669" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
<a id="2679" href="Effect.Functor.html#1149" class="Function">op</a> <a id="2682" class="Symbol">(</a><a id="2683" href="Algebra.Lattice.Bundles.html#5740" class="Field Operator">_∨_</a> <a id="2687" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2280" class="Function Operator">&lt;$&gt;₁</a> <a id="2692" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2172" class="Function Operator">⟦</a> <a id="2694" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2655" class="Bound">e₁</a> <a id="2697" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2172" class="Function Operator">⟧₁</a> <a id="2700" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2665" class="Bound">ρ</a> <a id="2702" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2295" class="Function Operator">⊛₁</a> <a id="2705" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2172" class="Function Operator">⟦</a> <a id="2707" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2661" class="Bound">e₂</a> <a id="2710" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2172" class="Function Operator">⟧₁</a> <a id="2713" href="Algebra.Lattice.Properties.BooleanAlgebra.Expression.html#2665" class="Bound">ρ</a><a id="2714" class="Symbol">)</a> <a id="2738" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2741" href="Effect.Applicative.html#3541" class="Function">op-⊛</a> <a id="2746" class="Symbol">_</a> <a id="2748" class="Symbol">_</a> <a id="2750" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
Expand Down
Loading

0 comments on commit 70e1607

Please sign in to comment.