Data.Fin.Patterns.html

<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Fin.Patterns</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><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">-- Patterns for Fin</a>
<a id="126" class="Comment">------------------------------------------------------------------------</a>

<a id="200" class="Symbol">{-#</a> <a id="204" class="Keyword">OPTIONS</a> <a id="212" class="Pragma">--without-K</a> <a id="224" class="Pragma">--safe</a> <a id="231" class="Symbol">#-}</a>

<a id="236" class="Keyword">module</a> <a id="243" href="Data.Fin.Patterns.html" class="Module">Data.Fin.Patterns</a> <a id="261" class="Keyword">where</a>

<a id="268" class="Keyword">open</a> <a id="273" class="Keyword">import</a> <a id="280" href="Data.Fin.Base.html" class="Module">Data.Fin.Base</a>

<a id="295" class="Comment">------------------------------------------------------------------------</a>
<a id="368" class="Comment">-- Constants</a>

<a id="382" class="Keyword">pattern</a> <a id="0F"></a><a id="390" href="Data.Fin.Patterns.html#390" class="InductiveConstructor">0F</a> <a id="393" class="Symbol">=</a> <a id="395" href="Data.Fin.Base.html#1148" class="InductiveConstructor">zero</a>
<a id="400" class="Keyword">pattern</a> <a id="1F"></a><a id="408" href="Data.Fin.Patterns.html#408" class="InductiveConstructor">1F</a> <a id="411" class="Symbol">=</a> <a id="413" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="417" href="Data.Fin.Patterns.html#390" class="InductiveConstructor">0F</a>
<a id="420" class="Keyword">pattern</a> <a id="2F"></a><a id="428" href="Data.Fin.Patterns.html#428" class="InductiveConstructor">2F</a> <a id="431" class="Symbol">=</a> <a id="433" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="437" href="Data.Fin.Patterns.html#408" class="InductiveConstructor">1F</a>
<a id="440" class="Keyword">pattern</a> <a id="3F"></a><a id="448" href="Data.Fin.Patterns.html#448" class="InductiveConstructor">3F</a> <a id="451" class="Symbol">=</a> <a id="453" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="457" href="Data.Fin.Patterns.html#428" class="InductiveConstructor">2F</a>
<a id="460" class="Keyword">pattern</a> <a id="4F"></a><a id="468" href="Data.Fin.Patterns.html#468" class="InductiveConstructor">4F</a> <a id="471" class="Symbol">=</a> <a id="473" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="477" href="Data.Fin.Patterns.html#448" class="InductiveConstructor">3F</a>
<a id="480" class="Keyword">pattern</a> <a id="5F"></a><a id="488" href="Data.Fin.Patterns.html#488" class="InductiveConstructor">5F</a> <a id="491" class="Symbol">=</a> <a id="493" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="497" href="Data.Fin.Patterns.html#468" class="InductiveConstructor">4F</a>
<a id="500" class="Keyword">pattern</a> <a id="6F"></a><a id="508" href="Data.Fin.Patterns.html#508" class="InductiveConstructor">6F</a> <a id="511" class="Symbol">=</a> <a id="513" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="517" href="Data.Fin.Patterns.html#488" class="InductiveConstructor">5F</a>
<a id="520" class="Keyword">pattern</a> <a id="7F"></a><a id="528" href="Data.Fin.Patterns.html#528" class="InductiveConstructor">7F</a> <a id="531" class="Symbol">=</a> <a id="533" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="537" href="Data.Fin.Patterns.html#508" class="InductiveConstructor">6F</a>
<a id="540" class="Keyword">pattern</a> <a id="8F"></a><a id="548" href="Data.Fin.Patterns.html#548" class="InductiveConstructor">8F</a> <a id="551" class="Symbol">=</a> <a id="553" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="557" href="Data.Fin.Patterns.html#528" class="InductiveConstructor">7F</a>
<a id="560" class="Keyword">pattern</a> <a id="9F"></a><a id="568" href="Data.Fin.Patterns.html#568" class="InductiveConstructor">9F</a> <a id="571" class="Symbol">=</a> <a id="573" href="Data.Fin.Base.html#1179" class="InductiveConstructor">suc</a> <a id="577" href="Data.Fin.Patterns.html#548" class="InductiveConstructor">8F</a>
</pre></body></html>