*** latex/PiWare/Circuit/Core.tex	2014-08-24 00:05:13.989362700 +0200
--- latex/PiWare/Circuit/Core.patched.tex	2014-08-24 00:04:56.863392100 +0200
***************
*** 57,86 ****
  %
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
! \>[4]\AgdaInductiveConstructor{DelayLoop} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i} \AgdaBound{o} \AgdaBound{l}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaBound{c} \AgdaSymbol{:} \AgdaDatatype{ℂ'} \AgdaSymbol{(}\AgdaBound{i} \AgdaPrimitive{+} \AgdaBound{l}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{o} \AgdaPrimitive{+} \AgdaBound{l}\AgdaSymbol{))} \AgdaSymbol{\{}\AgdaBound{p} \AgdaSymbol{:} \AgdaFunction{comb'} \AgdaBound{c}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i} \AgdaBound{o}\<%
  \\
  %
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
  \>[4]\AgdaInductiveConstructor{\_⟫'\_} \<[11]%
! \>[11]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i} \AgdaBound{m} \AgdaBound{o}\AgdaSymbol{\}} \<[30]%
! \>[30]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i} \AgdaBound{m} \<[42]%
! \>[42]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{m} \AgdaBound{o} \<[54]%
! \>[54]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i} \AgdaBound{o}\<%
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
  \>[4]\AgdaInductiveConstructor{\_|'\_} \<[11]%
! \>[11]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i₁} \AgdaBound{o₁} \AgdaBound{i₂} \AgdaBound{o₂}\AgdaSymbol{\}} \<[30]%
! \>[30]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i₁} \AgdaBound{o₁} \<[42]%
! \>[42]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i₂} \AgdaBound{o₂} \<[54]%
! \>[54]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaSymbol{(}\AgdaBound{i₁} \AgdaPrimitive{+} \AgdaBound{i₂}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{o₁} \AgdaPrimitive{+} \AgdaBound{o₂}\AgdaSymbol{)}\<%
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
  \>[4]\AgdaInductiveConstructor{\_|+'\_} \<[11]%
! \>[11]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{i₁} \AgdaBound{i₂} \AgdaBound{o}\AgdaSymbol{\}} \<[30]%
! \>[30]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i₁} \AgdaBound{o} \<[42]%
! \>[42]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i₂} \AgdaBound{o} \<[54]%
! \>[54]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaSymbol{(}\AgdaBound{i₁} \AgdaFunction{⊔} \AgdaBound{i₂}\AgdaSymbol{))} \AgdaBound{o}\<%
  \end{code}
  %</Circuit-core>
  
--- 57,83 ----
  %
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
! \>[4]\AgdaInductiveConstructor{DelayLoop} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{c} \AgdaSymbol{:} \AgdaDatatype{ℂ'} \AgdaSymbol{(}\AgdaBound{i} \AgdaPrimitive{+} \AgdaBound{l}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{o} \AgdaPrimitive{+} \AgdaBound{l}\AgdaSymbol{))} \AgdaSymbol{\{}\AgdaFunction{comb'} \AgdaBound{c}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i} \AgdaBound{o}\<%
  \\
  %
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
  \>[4]\AgdaInductiveConstructor{\_⟫'\_} \<[11]%
! \>[11]\AgdaSymbol{:} \AgdaDatatype{ℂ'} \AgdaBound{i} \AgdaBound{m} \<[30]%
! \>[30]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{m} \AgdaBound{o} \<[42]%
! \>[42]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i} \AgdaBound{o}\<%
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
  \>[4]\AgdaInductiveConstructor{\_|'\_} \<[11]%
! \>[11]\AgdaSymbol{:} \AgdaDatatype{ℂ'} \AgdaBound{i₁} \AgdaBound{o₁} \<[30]%
! \>[30]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i₂} \AgdaBound{o₂} \<[42]%
! \>[42]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaSymbol{(}\AgdaBound{i₁} \AgdaPrimitive{+} \AgdaBound{i₂}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{o₁} \AgdaPrimitive{+} \AgdaBound{o₂}\AgdaSymbol{)}\<%
  \\
  \>[0]\AgdaIndent{4}{}\<[4]%
  \>[4]\AgdaInductiveConstructor{\_|+'\_} \<[11]%
! \>[11]\AgdaSymbol{:} \AgdaDatatype{ℂ'} \AgdaBound{i₁} \AgdaBound{o} \<[30]%
! \>[30]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaBound{i₂} \AgdaBound{o} \<[42]%
! \>[42]\AgdaSymbol{→} \AgdaDatatype{ℂ'} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaSymbol{(}\AgdaBound{i₁} \AgdaFunction{⊔} \AgdaBound{i₂}\AgdaSymbol{))} \AgdaBound{o}\<%
  \end{code}
  %</Circuit-core>
  
