Index of /~nad/listings/codata

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.css 31-Aug-2017 14:34 1.2K 
[TXT]Stream.html 31-Aug-2017 14:34 1.6K 
[TXT]Data.Char.Core.html 31-Aug-2017 14:34 1.8K 
[TXT]Agda.Builtin.Unit.html 31-Aug-2017 14:34 1.9K 
[TXT]Foreign.Haskell.html 31-Aug-2017 14:34 2.2K 
[TXT]Agda.Builtin.IO.html 31-Aug-2017 14:34 2.3K 
[TXT]Agda.Builtin.TrustMe..>31-Aug-2017 14:34 2.6K 
[TXT]Data.Unit.Base.html 31-Aug-2017 14:34 2.8K 
[TXT]Data.Empty.html 31-Aug-2017 14:34 3.1K 
[TXT]Data.Bool.Show.html 31-Aug-2017 14:34 3.2K 
[TXT]Agda.Builtin.Equalit..>31-Aug-2017 14:34 3.2K 
[TXT]Agda.Builtin.Bool.html 31-Aug-2017 14:34 3.4K 
[TXT]Relation.Binary.Part..>31-Aug-2017 14:34 3.5K 
[TXT]Data.Bool.html 31-Aug-2017 14:34 3.5K 
[TXT]Category.Functor.Ide..>31-Aug-2017 14:34 4.0K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 4.0K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 4.1K 
[TXT]Level.html 31-Aug-2017 14:34 4.2K 
[TXT]Algebra.RingSolver.S..>31-Aug-2017 14:34 4.5K 
[TXT]Category.Monad.Ident..>31-Aug-2017 14:34 4.6K 
[TXT]Algebra.FunctionProp..>31-Aug-2017 14:34 4.8K 
[TXT]Relation.Binary.EqRe..>31-Aug-2017 14:34 4.8K 
[TXT]Agda.Builtin.Char.html 31-Aug-2017 14:34 4.8K 
[TXT]Agda.Builtin.Coinduc..>31-Aug-2017 14:34 5.2K 
[TXT]Category.Applicative..>31-Aug-2017 14:34 5.5K 
[TXT]Relation.Nullary.html 31-Aug-2017 14:34 5.5K 
[TXT]Data.Char.Base.html 31-Aug-2017 14:34 5.6K 
[TXT]Agda.Builtin.List.html 31-Aug-2017 14:34 5.9K 
[TXT]Coinduction.html 31-Aug-2017 14:34 6.1K 
[TXT]Relation.Binary.Prop..>31-Aug-2017 14:34 6.1K 
[TXT]TotalRecognisers.html 31-Aug-2017 14:34 6.2K 
[TXT]Agda.Builtin.Strict...>31-Aug-2017 14:34 6.2K 
[TXT]Data.Nat.html 31-Aug-2017 14:34 6.7K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 6.8K 
[TXT]Relation.Binary.Prop..>31-Aug-2017 14:34 6.9K 
[TXT]Agda.Builtin.String...>31-Aug-2017 14:34 6.9K 
[TXT]Relation.Nullary.Pro..>31-Aug-2017 14:34 7.2K 
[TXT]Relation.Binary.Hete..>31-Aug-2017 14:34 7.7K 
[TXT]RecursiveTypes.html 31-Aug-2017 14:34 8.0K 
[TXT]Relation.Binary.Cons..>31-Aug-2017 14:34 8.3K 
[TXT]Data.Nat.Show.html 31-Aug-2017 14:34 8.6K 
[TXT]Data.Unit.NonEta.html 31-Aug-2017 14:34 8.9K 
[TXT]RecursiveTypes.Seman..>31-Aug-2017 14:34 9.0K 
[TXT]Strict.html 31-Aug-2017 14:34 9.3K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 9.4K 
[TXT]Relation.Binary.Simp..>31-Aug-2017 14:34 10K 
[TXT]Mixfix.html 31-Aug-2017 14:34 10K 
[TXT]Operational-semantic..>31-Aug-2017 14:34 11K 
[TXT]Lambda.html 31-Aug-2017 14:34 11K 
[TXT]Mixfix.Cyclic.Preced..>31-Aug-2017 14:34 11K 
[TXT]Mixfix.Acyclic.Prece..>31-Aug-2017 14:34 11K 
[TXT]Relation.Binary.Inde..>31-Aug-2017 14:34 11K 
[TXT]Category.Functor.html 31-Aug-2017 14:34 13K 
[TXT]Category.Monad.html 31-Aug-2017 14:34 13K 
[TXT]Mixfix.Operator.html 31-Aug-2017 14:34 13K 
[TXT]Data.String.Base.html 31-Aug-2017 14:34 13K 
[TXT]Relation.Binary.Prop..>31-Aug-2017 14:34 13K 
[TXT]README.html 31-Aug-2017 14:34 14K 
[TXT]Data.Unit.html 31-Aug-2017 14:34 14K 
[TXT]Relation.Binary.Indu..>31-Aug-2017 14:34 15K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 15K 
[TXT]Data.BoundedVec.Inef..>31-Aug-2017 14:34 15K 
[TXT]Data.Char.html 31-Aug-2017 14:34 15K 
[TXT]TotalRecognisers.Sim..>31-Aug-2017 14:34 15K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 16K 
[TXT]Data.Bool.Base.html 31-Aug-2017 14:34 16K 
[TXT]Lambda.Substitution...>31-Aug-2017 14:34 17K 
[TXT]Data.Fin.Substitutio..>31-Aug-2017 14:34 17K 
[TXT]IO.Primitive.html 31-Aug-2017 14:34 17K 
[TXT]Mixfix.Acyclic.Lemma..>31-Aug-2017 14:34 18K 
[TXT]Relation.Binary.Preo..>31-Aug-2017 14:34 18K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 19K 
[TXT]Data.Conat.html 31-Aug-2017 14:34 19K 
[TXT]Lambda.Substitution...>31-Aug-2017 14:34 20K 
[TXT]Data.String.html 31-Aug-2017 14:34 20K 
[TXT]RecursiveTypes.Synta..>31-Aug-2017 14:34 20K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 21K 
[TXT]Data.List.Reverse.html 31-Aug-2017 14:34 22K 
[TXT]Function.Injection.html31-Aug-2017 14:34 23K 
[TXT]Mixfix.Fixity.html 31-Aug-2017 14:34 23K 
[TXT]Induction.html 31-Aug-2017 14:34 23K 
[TXT]Agda.Builtin.Nat.html 31-Aug-2017 14:34 23K 
[TXT]Lambda.Substitution...>31-Aug-2017 14:34 24K 
[TXT]Agda.Primitive.html 31-Aug-2017 14:34 24K 
[TXT]Data.List.NonEmpty.P..>31-Aug-2017 14:34 25K 
[TXT]Contractive.Function..>31-Aug-2017 14:34 25K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 25K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 25K 
[TXT]Algebra.RingSolver.N..>31-Aug-2017 14:34 26K 
[TXT]Data.List.Any.Member..>31-Aug-2017 14:34 26K 
[TXT]Tree.html 31-Aug-2017 14:34 26K 
[TXT]Algebra.Properties.A..>31-Aug-2017 14:34 26K 
[TXT]Data.List.Any.Member..>31-Aug-2017 14:34 27K 
[TXT]DataAndCodata.html 31-Aug-2017 14:34 29K 
[TXT]Data.List.html 31-Aug-2017 14:34 29K 
[TXT]Data.DifferenceList...>31-Aug-2017 14:34 29K 
[TXT]UniverseIndex.html 31-Aug-2017 14:34 30K 
[TXT]Data.List.Any.html 31-Aug-2017 14:34 30K 
[TXT]Data.Product.N-ary.html31-Aug-2017 14:34 30K 
[TXT]Function.Bijection.html31-Aug-2017 14:34 30K 
[TXT]Relation.Binary.Inde..>31-Aug-2017 14:34 30K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 31K 
[TXT]Algebra.Morphism.html 31-Aug-2017 14:34 32K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 32K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 33K 
[TXT]Algebra.Properties.R..>31-Aug-2017 14:34 33K 
[TXT]Function.Surjection...>31-Aug-2017 14:34 35K 
[TXT]Category.Monad.Index..>31-Aug-2017 14:34 35K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 35K 
[TXT]Data.List.All.html 31-Aug-2017 14:34 36K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 38K 
[TXT]Mixfix.Cyclic.Gramma..>31-Aug-2017 14:34 39K 
[TXT]Mixfix.Acyclic.Gramm..>31-Aug-2017 14:34 39K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 39K 
[TXT]BreadthFirst.Univers..>31-Aug-2017 14:34 40K 
[TXT]TotalRecognisers.Sim..>31-Aug-2017 14:34 40K 
[TXT]Data.Sum.html 31-Aug-2017 14:34 41K 
[TXT]Data.Nat.InfinitelyO..>31-Aug-2017 14:34 41K 
[TXT]Data.List.Any.Member..>31-Aug-2017 14:34 43K 
[TXT]Stream.Programs.html 31-Aug-2017 14:34 43K 
[TXT]Data.Maybe.Base.html 31-Aug-2017 14:34 43K 
[TXT]IO.html 31-Aug-2017 14:34 43K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 43K 
[TXT]LargeCombinators.html 31-Aug-2017 14:34 44K 
[TXT]Algebra.Properties.D..>31-Aug-2017 14:34 44K 
[TXT]Algebra.Properties.G..>31-Aug-2017 14:34 45K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 45K 
[TXT]Relation.Binary.Refl..>31-Aug-2017 14:34 46K 
[TXT]Lambda.Syntax.html 31-Aug-2017 14:34 46K 
[TXT]Data.Digit.html 31-Aug-2017 14:34 47K 
[TXT]MuNu.html 31-Aug-2017 14:34 47K 
[TXT]Category.Applicative..>31-Aug-2017 14:34 47K 
[TXT]Relation.Binary.NonS..>31-Aug-2017 14:34 47K 
[TXT]Mixfix.Expr.html 31-Aug-2017 14:34 47K 
[TXT]Function.LeftInverse..>31-Aug-2017 14:34 48K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 49K 
[TXT]Function.Equality.html 31-Aug-2017 14:34 49K 
[TXT]Function.Equivalence..>31-Aug-2017 14:34 50K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 50K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 51K 
[TXT]Relation.Nullary.Dec..>31-Aug-2017 14:34 51K 
[TXT]Algebra.RingSolver.A..>31-Aug-2017 14:34 52K 
[TXT]Lambda.Closure.Funct..>31-Aug-2017 14:34 54K 
[TXT]InductiveStreamEqual..>31-Aug-2017 14:34 56K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 56K 
[TXT]Algebra.FunctionProp..>31-Aug-2017 14:34 57K 
[TXT]Function.html 31-Aug-2017 14:34 59K 
[TXT]Data.Maybe.html 31-Aug-2017 14:34 60K 
[TXT]BreadthFirstWithoutP..>31-Aug-2017 14:34 60K 
[TXT]Contractive.Stream.html31-Aug-2017 14:34 60K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 61K 
[TXT]Category.Monad.State..>31-Aug-2017 14:34 61K 
[TXT]Data.Fin.Substitutio..>31-Aug-2017 14:34 62K 
[TXT]Data.Vec.Equality.html 31-Aug-2017 14:34 63K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 64K 
[TXT]Algebra.Monoid-solve..>31-Aug-2017 14:34 64K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 64K 
[TXT]Hinze.Lemmas.html 31-Aug-2017 14:34 64K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 65K 
[TXT]TotalRecognisers.Sim..>31-Aug-2017 14:34 66K 
[TXT]RecursiveTypes.Synta..>31-Aug-2017 14:34 66K 
[TXT]Mixfix.Acyclic.Examp..>31-Aug-2017 14:34 66K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 67K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 67K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 68K 
[TXT]Hinze.Simplified.Sec..>31-Aug-2017 14:34 68K 
[TXT]Lambda.Substitution...>31-Aug-2017 14:34 68K 
[TXT]Mixfix.Cyclic.Exampl..>31-Aug-2017 14:34 68K 
[TXT]Function.Inverse.html 31-Aug-2017 14:34 68K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 69K 
[TXT]Contractive.Examples..>31-Aug-2017 14:34 69K 
[TXT]Algebra.FunctionProp..>31-Aug-2017 14:34 70K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 70K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 70K 
[TXT]BreadthFirst.html 31-Aug-2017 14:34 71K 
[TXT]Data.Nat.Base.html 31-Aug-2017 14:34 71K 
[TXT]Data.Star.html 31-Aug-2017 14:34 73K 
[TXT]MapIterate.html 31-Aug-2017 14:34 74K 
[TXT]Data.Product.html 31-Aug-2017 14:34 75K 
[TXT]Data.Nat.DivMod.html 31-Aug-2017 14:34 75K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 75K 
[TXT]Stream.Equality.html 31-Aug-2017 14:34 75K 
[TXT]Induction.WellFounde..>31-Aug-2017 14:34 76K 
[TXT]Data.Star.Properties..>31-Aug-2017 14:34 76K 
[TXT]BreadthFirst.Program..>31-Aug-2017 14:34 76K 
[TXT]Contractive.html 31-Aug-2017 14:34 78K 
[TXT]RecursiveTypes.Subte..>31-Aug-2017 14:34 79K 
[TXT]Hinze.Simplified.Sec..>31-Aug-2017 14:34 83K 
[TXT]RecursiveTypes.Subst..>31-Aug-2017 14:34 84K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 84K 
[TXT]Algebra.Operations.html31-Aug-2017 14:34 84K 
[TXT]Algebra.Properties.L..>31-Aug-2017 14:34 85K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 85K 
[TXT]Hinze.Section3.html 31-Aug-2017 14:34 86K 
[TXT]Relation.Nullary.Uni..>31-Aug-2017 14:34 86K 
[TXT]Data.Stream.html 31-Aug-2017 14:34 88K 
[TXT]StreamProg.html 31-Aug-2017 14:34 89K 
[TXT]Induction.Nat.html 31-Aug-2017 14:34 90K 
[TXT]Mixfix.Cyclic.Show.html31-Aug-2017 14:34 90K 
[TXT]Relation.Nullary.Neg..>31-Aug-2017 14:34 91K 
[TXT]Relation.Binary.Core..>31-Aug-2017 14:34 92K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 92K 
[TXT]Relation.Unary.html 31-Aug-2017 14:34 93K 
[TXT]Relation.Binary.Cons..>31-Aug-2017 14:34 94K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 100K 
[TXT]Hinze.Section2-4.html 31-Aug-2017 14:34 101K 
[TXT]Relation.Binary.Latt..>31-Aug-2017 14:34 101K 
[TXT]Stream.Pointwise.html 31-Aug-2017 14:34 101K 
[TXT]ThueMorseLeq.html 31-Aug-2017 14:34 103K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 105K 
[TXT]VenanziosProblem.html 31-Aug-2017 14:34 108K 
[TXT]Relation.Binary.Prop..>31-Aug-2017 14:34 109K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 109K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 109K 
[TXT]Data.Fin.html 31-Aug-2017 14:34 110K 
[TXT]Relation.Binary.On.html31-Aug-2017 14:34 113K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 113K 
[TXT]Mixfix.Acyclic.Show...>31-Aug-2017 14:34 113K 
[TXT]Category.Monad.Parti..>31-Aug-2017 14:34 116K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 116K 
[TXT]Data.Bool.Properties..>31-Aug-2017 14:34 117K 
[TXT]Algebra.RingSolver.L..>31-Aug-2017 14:34 118K 
[TXT]ArbitraryChunks.html 31-Aug-2017 14:34 119K 
[TXT]Data.Vec.N-ary.html 31-Aug-2017 14:34 122K 
[TXT]Lambda.Closure.Relat..>31-Aug-2017 14:34 124K 
[TXT]Lambda.Substitution...>31-Aug-2017 14:34 125K 
[TXT]Relation.Binary.html 31-Aug-2017 14:34 126K 
[TXT]Data.List.Countdown...>31-Aug-2017 14:34 127K 
[TXT]Algebra.html 31-Aug-2017 14:34 129K 
[TXT]Relation.Binary.List..>31-Aug-2017 14:34 132K 
[TXT]TotalRecognisers.Sim..>31-Aug-2017 14:34 136K 
[TXT]Nested.html 31-Aug-2017 14:34 136K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 139K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 141K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 143K 
[TXT]SingletonChunks.html 31-Aug-2017 14:34 144K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 146K 
[TXT]Data.List.Base.html 31-Aug-2017 14:34 148K 
[TXT]Relation.Binary.Hete..>31-Aug-2017 14:34 151K 
[TXT]Lambda.Closure.Funct..>31-Aug-2017 14:34 155K 
[TXT]Data.Vec.html 31-Aug-2017 14:34 159K 
[TXT]Mixfix.Equivalence.html31-Aug-2017 14:34 161K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 162K 
[TXT]Function.Related.html 31-Aug-2017 14:34 163K 
[TXT]Algebra.Structures.html31-Aug-2017 14:34 166K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 174K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 175K 
[TXT]Data.List.NonEmpty.html31-Aug-2017 14:34 178K 
[TXT]Relation.Binary.List..>31-Aug-2017 14:34 182K 
[TXT]Lambda.Closure.Equiv..>31-Aug-2017 14:34 188K 
[TXT]StructurallyRecursiv..>31-Aug-2017 14:34 191K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 193K 
[TXT]RecursiveTypes.Subty..>31-Aug-2017 14:34 199K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 201K 
[TXT]Data.List.Any.BagAnd..>31-Aug-2017 14:34 202K 
[TXT]AdmissibleButNotPost..>31-Aug-2017 14:34 212K 
[TXT]Data.List.Any.Member..>31-Aug-2017 14:34 219K 
[TXT]Mixfix.Cyclic.Unique..>31-Aug-2017 14:34 222K 
[TXT]BreadthFirst.Lemmas...>31-Aug-2017 14:34 228K 
[TXT]Data.Fin.Properties...>31-Aug-2017 14:34 230K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 233K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 234K 
[TXT]Lambda.Closure.Equiv..>31-Aug-2017 14:34 238K 
[TXT]Lambda.Closure.Funct..>31-Aug-2017 14:34 243K 
[TXT]RecursiveTypes.Subte..>31-Aug-2017 14:34 252K 
[TXT]Mixfix.Cyclic.Lib.html 31-Aug-2017 14:34 259K 
[TXT]Relation.Binary.Prod..>31-Aug-2017 14:34 264K 
[TXT]ThueMorse.html 31-Aug-2017 14:34 265K 
[TXT]Data.Colist.html 31-Aug-2017 14:34 277K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 281K 
[TXT]Mixfix.Acyclic.Lib.html31-Aug-2017 14:34 281K 
[TXT]Lambda.VirtualMachin..>31-Aug-2017 14:34 287K 
[TXT]Relation.Binary.Sigm..>31-Aug-2017 14:34 288K 
[TXT]Function.Related.Typ..>31-Aug-2017 14:34 290K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 297K 
[TXT]TotalParserCombinato..>31-Aug-2017 14:34 302K 
[TXT]InfinitelyOften.html 31-Aug-2017 14:34 312K 
[TXT]TotalRecognisers.Lef..>31-Aug-2017 14:34 313K 
[TXT]Lambda.Closure.Funct..>31-Aug-2017 14:34 363K 
[TXT]Relation.Binary.Sum...>31-Aug-2017 14:34 376K 
[TXT]Lambda.Closure.Funct..>31-Aug-2017 14:34 377K 
[TXT]Algebra.RingSolver.html31-Aug-2017 14:34 382K 
[TXT]Algebra.Properties.B..>31-Aug-2017 14:34 385K 
[TXT]Data.Fin.Substitutio..>31-Aug-2017 14:34 392K 
[TXT]Data.Vec.Properties...>31-Aug-2017 14:34 427K 
[TXT]Data.List.Properties..>31-Aug-2017 14:34 463K 
[TXT]Data.List.Any.Proper..>31-Aug-2017 14:34 470K 
[TXT]Lambda.Closure.Funct..>31-Aug-2017 14:34 527K 
[TXT]Data.Nat.Properties...>31-Aug-2017 14:34 543K 
[TXT]Category.Monad.Parti..>31-Aug-2017 14:34 583K 

README
------------------------------------------------------------------------
-- Code related to the paper Mixing Induction and Coinduction
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module README where

------------------------------------------------------------------------
-- Section 3: An ad-hoc method for making corecursive definitions
-- guarded

-- A definition of the stream of Fibonacci numbers, as well
-- as a definition of the Hamming numbers.

import StreamProg

-- Proofs of the map-iterate property and iterate fusion.

import MapIterate

-- A somewhat more elaborate/complicated variant of the method which
-- can handle functions like tail.

import SingletonChunks

-- A generalised variant of (parts of) SingletonChunks, plus some
-- extra examples.

import ArbitraryChunks

-- Implementations of the Thue-Morse sequence, using non-uniform chunk
-- sizes.

import ThueMorse
import ThueMorseLeq

-- Another variant which can handle tail. I believe that this one has
-- limited applicability.

import LargeCombinators

-- An example which shows that nested applications of the defined
-- function can be handled.

import Nested

-- A formalisation of parts of Ralf Hinze's paper "Streams and Unique
-- Fixed Points".

import Stream
import Stream.Programs
import Stream.Equality
import Stream.Pointwise
import Hinze.Lemmas
import Hinze.Section2-4
import Hinze.Section3
import Hinze.Simplified.Section2-4
import Hinze.Simplified.Section3

-- By indexing the program and WHNF types on a universe one can handle
-- several types at the same time.

import UniverseIndex

-- Breadth-first labelling of trees, /almost/ implementing the classic
-- tie-the-recursive-knot algorithm due to Jeremy Gibbons and Geraint
-- Jones (see "Linear-time Breadth-first Tree Algorithms: An Exercise
-- in the Arithmetic of Folds and Zips", or Chris Okasaki's
-- explanation in "Breadth-First Numbering: Lessons from a Small
-- Exercise in Algorithm Design"). Proper sharing is not maintained,
-- though, so this implementation is far from being linear in the size
-- of the tree.

import Stream
import Tree
import BreadthFirst.Universe
import BreadthFirst.Programs
import BreadthFirst

-- A simplified variant of the code above, without any correctness
-- statement or proof.

import BreadthFirstWithoutProof

-- A solution to a problem posed by Venanzio Capretta: The equation
--
--   φ s = s ⋎ φ (evens (φ s))
--
-- has at most one solution. (Notice the nested uses of φ, and the use
-- of evens which removes every other element from its input.)

import VenanziosProblem

-- A sound, inductive approximation of stream equality.

import InductiveStreamEquality

------------------------------------------------------------------------
-- Section 4: Subtyping for recursive types

-- Formalisation of subtyping for recursive types, partly based on
-- "Coinductive Axiomatization of Recursive Type Equality and
-- Subtyping" by Michael Brandt and Fritz Henglein.

import RecursiveTypes

-- One must exercise caution when using the technique advertised in
-- Section 4. The following module shows that, in a coinductive
-- setting, it is not always sound to postulate admissible rules
-- (inductively).

import AdmissibleButNotPostulable

------------------------------------------------------------------------
-- Section 5: Total parser combinators

-- The following code may not match the paper exactly. See the paper
-- Total Parser Combinators for more information.

import TotalParserCombinators

------------------------------------------------------------------------
-- Section 6: Big-step semantics for both converging and diverging
-- computations

-- A definition of a big-step semantics which handles termination and
-- non-termination at the same time, without duplication of rules.
-- Partly based on Leroy and Grall's "Coinductive big-step operational
-- semantics" and Cousot and Cousot's "Bi-inductive structural
-- semantics".

import Lambda

-- An example showing how the list and colist types can be "unified".

import DataAndCodata

------------------------------------------------------------------------
-- Section 7: Related work

-- An investigation of nested fixpoints of the form μX.νY.… in Agda.
-- It turns out that they cannot be represented directly.

import MuNu

-- An implementation of "A Unifying Approach to Recursive and
-- Co-recursive Definitions" by Pietro Di Gianantonio and Marino
-- Miculan. Contains one postulate.

import Contractive
import Contractive.Function
import Contractive.Stream
import Contractive.Examples

------------------------------------------------------------------------
-- Code which is not directly related to any particular section in the
-- paper

-- Various definitions of "true infinitely often", along with
-- comparisons of the definitions.

import InfinitelyOften