Index of /~nad/listings/codata

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]AdmissibleButNotPost..>20-Mar-2018 18:41 158K 
[TXT]Agda.Builtin.Bool.html 20-Mar-2018 18:41 2.4K 
[TXT]Agda.Builtin.Char.html 20-Mar-2018 18:41 3.7K 
[TXT]Agda.Builtin.Coinduc..>20-Mar-2018 18:41 3.7K 
[TXT]Agda.Builtin.Equalit..>20-Mar-2018 18:41 2.3K 
[TXT]Agda.Builtin.IO.html 20-Mar-2018 18:41 1.5K 
[TXT]Agda.Builtin.List.html 20-Mar-2018 18:41 3.6K 
[TXT]Agda.Builtin.Nat.html 20-Mar-2018 18:41 18K 
[TXT]Agda.Builtin.Strict...>20-Mar-2018 18:41 4.5K 
[TXT]Agda.Builtin.String...>20-Mar-2018 18:41 5.1K 
[TXT]Agda.Builtin.TrustMe..>20-Mar-2018 18:41 1.8K 
[TXT]Agda.Builtin.Unit.html 20-Mar-2018 18:41 1.2K 
[TXT]Agda.Primitive.Cubic..>20-Mar-2018 18:41 15K 
[TXT]Agda.Primitive.html 20-Mar-2018 18:41 3.6K 
[TXT]Agda.css 20-Mar-2018 18:41 1.2K 
[TXT]Algebra.FunctionProp..>20-Mar-2018 18:41 56K 
[TXT]Algebra.FunctionProp..>20-Mar-2018 18:41 3.5K 
[TXT]Algebra.FunctionProp..>20-Mar-2018 18:41 44K 
[TXT]Algebra.Monoid-solve..>20-Mar-2018 18:41 48K 
[TXT]Algebra.Morphism.html 20-Mar-2018 18:41 45K 
[TXT]Algebra.Operations.html20-Mar-2018 18:41 64K 
[TXT]Algebra.Properties.A..>20-Mar-2018 18:41 20K 
[TXT]Algebra.Properties.B..>20-Mar-2018 18:41 298K 
[TXT]Algebra.Properties.D..>20-Mar-2018 18:41 34K 
[TXT]Algebra.Properties.G..>20-Mar-2018 18:41 35K 
[TXT]Algebra.Properties.L..>20-Mar-2018 18:41 66K 
[TXT]Algebra.Properties.R..>20-Mar-2018 18:41 26K 
[TXT]Algebra.RingSolver.A..>20-Mar-2018 18:41 39K 
[TXT]Algebra.RingSolver.L..>20-Mar-2018 18:41 95K 
[TXT]Algebra.RingSolver.N..>20-Mar-2018 18:41 20K 
[TXT]Algebra.RingSolver.S..>20-Mar-2018 18:41 3.3K 
[TXT]Algebra.RingSolver.html20-Mar-2018 18:41 291K 
[TXT]Algebra.Structures.html20-Mar-2018 18:41 141K 
[TXT]Algebra.html 20-Mar-2018 18:41 93K 
[TXT]ArbitraryChunks.html 20-Mar-2018 18:41 90K 
[TXT]BreadthFirst.Lemmas...>20-Mar-2018 18:41 173K 
[TXT]BreadthFirst.Program..>20-Mar-2018 18:41 58K 
[TXT]BreadthFirst.Univers..>20-Mar-2018 18:41 31K 
[TXT]BreadthFirst.html 20-Mar-2018 18:41 53K 
[TXT]BreadthFirstWithoutP..>20-Mar-2018 18:41 46K 
[TXT]Category.Applicative..>20-Mar-2018 18:41 36K 
[TXT]Category.Applicative..>20-Mar-2018 18:41 3.9K 
[TXT]Category.Functor.html 20-Mar-2018 18:41 9.2K 
[TXT]Category.Monad.Ident..>20-Mar-2018 18:41 3.3K 
[TXT]Category.Monad.Index..>20-Mar-2018 18:41 27K 
[TXT]Category.Monad.Parti..>20-Mar-2018 18:41 89K 
[TXT]Category.Monad.Parti..>20-Mar-2018 18:41 443K 
[TXT]Category.Monad.State..>20-Mar-2018 18:41 46K 
[TXT]Category.Monad.html 20-Mar-2018 18:41 9.2K 
[TXT]Coinduction.html 20-Mar-2018 18:41 4.5K 
[TXT]Contractive.Examples..>20-Mar-2018 18:41 53K 
[TXT]Contractive.Function..>20-Mar-2018 18:41 19K 
[TXT]Contractive.Stream.html20-Mar-2018 18:41 45K 
[TXT]Contractive.html 20-Mar-2018 18:41 58K 
[TXT]Data.Bool.Base.html 20-Mar-2018 18:41 12K 
[TXT]Data.Bool.Properties..>20-Mar-2018 18:41 106K 
[TXT]Data.Bool.Show.html 20-Mar-2018 18:41 2.3K 
[TXT]Data.Bool.html 20-Mar-2018 18:41 2.5K 
[TXT]Data.BoundedVec.Inef..>20-Mar-2018 18:41 12K 
[TXT]Data.Char.Base.html 20-Mar-2018 18:41 8.1K 
[TXT]Data.Char.Core.html 20-Mar-2018 18:41 1.2K 
[TXT]Data.Char.html 20-Mar-2018 18:41 12K 
[TXT]Data.Colist.html 20-Mar-2018 18:41 229K 
[TXT]Data.Conat.html 20-Mar-2018 18:41 23K 
[TXT]Data.DifferenceList...>20-Mar-2018 18:41 22K 
[TXT]Data.Digit.html 20-Mar-2018 18:41 35K 
[TXT]Data.Empty.html 20-Mar-2018 18:41 2.2K 
[TXT]Data.Fin.Properties...>20-Mar-2018 18:41 163K 
[TXT]Data.Fin.Substitutio..>20-Mar-2018 18:41 299K 
[TXT]Data.Fin.Substitutio..>20-Mar-2018 18:41 13K 
[TXT]Data.Fin.Substitutio..>20-Mar-2018 18:41 47K 
[TXT]Data.Fin.html 20-Mar-2018 18:41 82K 
[TXT]Data.List.All.html 20-Mar-2018 18:41 27K 
[TXT]Data.List.Any.BagAnd..>20-Mar-2018 18:41 154K 
[TXT]Data.List.Any.Member..>20-Mar-2018 18:41 21K 
[TXT]Data.List.Any.Member..>20-Mar-2018 18:41 183K 
[TXT]Data.List.Any.Member..>20-Mar-2018 18:41 32K 
[TXT]Data.List.Any.Member..>20-Mar-2018 18:41 20K 
[TXT]Data.List.Any.Proper..>20-Mar-2018 18:41 359K 
[TXT]Data.List.Any.html 20-Mar-2018 18:41 22K 
[TXT]Data.List.Base.html 20-Mar-2018 18:41 121K 
[TXT]Data.List.Categorica..>20-Mar-2018 18:41 116K 
[TXT]Data.List.Countdown...>20-Mar-2018 18:41 96K 
[TXT]Data.List.NonEmpty.P..>20-Mar-2018 18:41 19K 
[TXT]Data.List.NonEmpty.html20-Mar-2018 18:41 135K 
[TXT]Data.List.Properties..>20-Mar-2018 18:41 273K 
[TXT]Data.List.Relation.L..>20-Mar-2018 18:41 62K 
[TXT]Data.List.Relation.P..>20-Mar-2018 18:41 101K 
[TXT]Data.List.Relation.S..>20-Mar-2018 18:41 84K 
[TXT]Data.List.Reverse.html 20-Mar-2018 18:41 16K 
[TXT]Data.List.html 20-Mar-2018 18:41 1.0K 
[TXT]Data.Maybe.Base.html 20-Mar-2018 18:41 35K 
[TXT]Data.Maybe.html 20-Mar-2018 18:41 45K 
[TXT]Data.Nat.Base.html 20-Mar-2018 18:41 54K 
[TXT]Data.Nat.DivMod.html 20-Mar-2018 18:41 57K 
[TXT]Data.Nat.InfinitelyO..>20-Mar-2018 18:41 32K 
[TXT]Data.Nat.Properties...>20-Mar-2018 18:41 463K 
[TXT]Data.Nat.Show.html 20-Mar-2018 18:41 6.3K 
[TXT]Data.Nat.html 20-Mar-2018 18:41 929  
[TXT]Data.Product.N-ary.html20-Mar-2018 18:41 23K 
[TXT]Data.Product.Relatio..>20-Mar-2018 18:41 199K 
[TXT]Data.Product.Relatio..>20-Mar-2018 18:41 226K 
[TXT]Data.Product.html 20-Mar-2018 18:41 56K 
[TXT]Data.Star.Properties..>20-Mar-2018 18:41 63K 
[TXT]Data.Star.html 20-Mar-2018 18:41 55K 
[TXT]Data.Stream.html 20-Mar-2018 18:41 66K 
[TXT]Data.String.Base.html 20-Mar-2018 18:41 9.7K 
[TXT]Data.String.html 20-Mar-2018 18:41 15K 
[TXT]Data.Sum.Relation.Ge..>20-Mar-2018 18:41 294K 
[TXT]Data.Sum.html 20-Mar-2018 18:41 30K 
[TXT]Data.Unit.Base.html 20-Mar-2018 18:41 1.9K 
[TXT]Data.Unit.NonEta.html 20-Mar-2018 18:41 6.7K 
[TXT]Data.Unit.html 20-Mar-2018 18:41 11K 
[TXT]Data.Vec.N-ary.html 20-Mar-2018 18:41 92K 
[TXT]Data.Vec.Properties...>20-Mar-2018 18:41 308K 
[TXT]Data.Vec.Relation.Eq..>20-Mar-2018 18:41 50K 
[TXT]Data.Vec.html 20-Mar-2018 18:41 117K 
[TXT]DataAndCodata.html 20-Mar-2018 18:41 22K 
[TXT]Foreign.Haskell.html 20-Mar-2018 18:41 1.6K 
[TXT]Function.Bijection.html20-Mar-2018 18:41 23K 
[TXT]Function.Equality.html 20-Mar-2018 18:41 37K 
[TXT]Function.Equivalence..>20-Mar-2018 18:41 37K 
[TXT]Function.Injection.html20-Mar-2018 18:41 17K 
[TXT]Function.Inverse.html 20-Mar-2018 18:41 51K 
[TXT]Function.LeftInverse..>20-Mar-2018 18:41 36K 
[TXT]Function.Related.Typ..>20-Mar-2018 18:41 220K 
[TXT]Function.Related.html 20-Mar-2018 18:41 123K 
[TXT]Function.Surjection...>20-Mar-2018 18:41 26K 
[TXT]Function.html 20-Mar-2018 18:41 43K 
[TXT]Hinze.Lemmas.html 20-Mar-2018 18:41 48K 
[TXT]Hinze.Section2-4.html 20-Mar-2018 18:41 75K 
[TXT]Hinze.Section3.html 20-Mar-2018 18:41 64K 
[TXT]Hinze.Simplified.Sec..>20-Mar-2018 18:41 64K 
[TXT]Hinze.Simplified.Sec..>20-Mar-2018 18:41 52K 
[TXT]IO.Primitive.html 20-Mar-2018 18:41 14K 
[TXT]IO.html 20-Mar-2018 18:41 33K 
[TXT]Induction.Nat.html 20-Mar-2018 18:41 66K 
[TXT]Induction.WellFounde..>20-Mar-2018 18:41 61K 
[TXT]Induction.html 20-Mar-2018 18:41 17K 
[TXT]InductiveStreamEqual..>20-Mar-2018 18:41 43K 
[TXT]InfinitelyOften.html 20-Mar-2018 18:41 233K 
[TXT]Lambda.Closure.Equiv..>20-Mar-2018 18:41 178K 
[TXT]Lambda.Closure.Equiv..>20-Mar-2018 18:41 144K 
[TXT]Lambda.Closure.Funct..>20-Mar-2018 18:41 277K 
[TXT]Lambda.Closure.Funct..>20-Mar-2018 18:41 119K 
[TXT]Lambda.Closure.Funct..>20-Mar-2018 18:41 302K 
[TXT]Lambda.Closure.Funct..>20-Mar-2018 18:41 412K 
[TXT]Lambda.Closure.Funct..>20-Mar-2018 18:41 42K 
[TXT]Lambda.Closure.Funct..>20-Mar-2018 18:41 183K 
[TXT]Lambda.Closure.Relat..>20-Mar-2018 18:41 93K 
[TXT]Lambda.Substitution...>20-Mar-2018 18:41 17K 
[TXT]Lambda.Substitution...>20-Mar-2018 18:41 51K 
[TXT]Lambda.Substitution...>20-Mar-2018 18:41 15K 
[TXT]Lambda.Substitution...>20-Mar-2018 18:41 13K 
[TXT]Lambda.Substitution...>20-Mar-2018 18:41 94K 
[TXT]Lambda.Syntax.html 20-Mar-2018 18:41 35K 
[TXT]Lambda.VirtualMachin..>20-Mar-2018 18:41 212K 
[TXT]Lambda.html 20-Mar-2018 18:41 8.9K 
[TXT]LargeCombinators.html 20-Mar-2018 18:41 33K 
[TXT]Level.html 20-Mar-2018 18:41 3.0K 
[TXT]MapIterate.html 20-Mar-2018 18:41 55K 
[TXT]Mixfix.Acyclic.Examp..>20-Mar-2018 18:41 51K 
[TXT]Mixfix.Acyclic.Gramm..>20-Mar-2018 18:41 30K 
[TXT]Mixfix.Acyclic.Lemma..>20-Mar-2018 18:41 13K 
[TXT]Mixfix.Acyclic.Lib.html20-Mar-2018 18:41 205K 
[TXT]Mixfix.Acyclic.Prece..>20-Mar-2018 18:41 8.6K 
[TXT]Mixfix.Acyclic.Show...>20-Mar-2018 18:41 83K 
[TXT]Mixfix.Cyclic.Exampl..>20-Mar-2018 18:41 52K 
[TXT]Mixfix.Cyclic.Gramma..>20-Mar-2018 18:41 30K 
[TXT]Mixfix.Cyclic.Lib.html 20-Mar-2018 18:41 187K 
[TXT]Mixfix.Cyclic.Preced..>20-Mar-2018 18:41 8.1K 
[TXT]Mixfix.Cyclic.Show.html20-Mar-2018 18:41 66K 
[TXT]Mixfix.Cyclic.Unique..>20-Mar-2018 18:41 154K 
[TXT]Mixfix.Equivalence.html20-Mar-2018 18:41 110K 
[TXT]Mixfix.Expr.html 20-Mar-2018 18:41 34K 
[TXT]Mixfix.Fixity.html 20-Mar-2018 18:41 17K 
[TXT]Mixfix.Operator.html 20-Mar-2018 18:41 9.5K 
[TXT]Mixfix.html 20-Mar-2018 18:41 8.3K 
[TXT]MuNu.html 20-Mar-2018 18:41 35K 
[TXT]Nested.html 20-Mar-2018 18:41 95K 
[TXT]Operational-semantic..>20-Mar-2018 18:41 8.5K 
[TXT]README.html 20-Mar-2018 18:41 11K 
[TXT]RecursiveTypes.Seman..>20-Mar-2018 18:41 6.7K 
[TXT]RecursiveTypes.Subst..>20-Mar-2018 18:41 63K 
[TXT]RecursiveTypes.Subte..>20-Mar-2018 18:41 60K 
[TXT]RecursiveTypes.Subte..>20-Mar-2018 18:41 189K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 80K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 83K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 153K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 5.0K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 89K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 51K 
[TXT]RecursiveTypes.Subty..>20-Mar-2018 18:41 26K 
[TXT]RecursiveTypes.Synta..>20-Mar-2018 18:41 15K 
[TXT]RecursiveTypes.Synta..>20-Mar-2018 18:41 50K 
[TXT]RecursiveTypes.html 20-Mar-2018 18:41 6.5K 
[TXT]Relation.Binary.Cons..>20-Mar-2018 18:41 6.3K 
[TXT]Relation.Binary.Cons..>20-Mar-2018 18:41 72K 
[TXT]Relation.Binary.Core..>20-Mar-2018 18:41 70K 
[TXT]Relation.Binary.EqRe..>20-Mar-2018 18:41 3.4K 
[TXT]Relation.Binary.Hete..>20-Mar-2018 18:41 5.8K 
[TXT]Relation.Binary.Hete..>20-Mar-2018 18:41 119K 
[TXT]Relation.Binary.Inde..>20-Mar-2018 18:41 23K 
[TXT]Relation.Binary.Inde..>20-Mar-2018 18:41 8.5K 
[TXT]Relation.Binary.Indu..>20-Mar-2018 18:41 11K 
[TXT]Relation.Binary.Latt..>20-Mar-2018 18:41 77K 
[TXT]Relation.Binary.List..>20-Mar-2018 18:41 1.1K 
[TXT]Relation.Binary.NonS..>20-Mar-2018 18:41 36K 
[TXT]Relation.Binary.On.html20-Mar-2018 18:41 85K 
[TXT]Relation.Binary.Part..>20-Mar-2018 18:41 2.6K 
[TXT]Relation.Binary.Preo..>20-Mar-2018 18:41 14K 
[TXT]Relation.Binary.Prod..>20-Mar-2018 18:41 1.1K 
[TXT]Relation.Binary.Prop..>20-Mar-2018 18:41 4.6K 
[TXT]Relation.Binary.Prop..>20-Mar-2018 18:41 10K 
[TXT]Relation.Binary.Prop..>20-Mar-2018 18:41 10K 
[TXT]Relation.Binary.Prop..>20-Mar-2018 18:41 78K 
[TXT]Relation.Binary.Refl..>20-Mar-2018 18:41 36K 
[TXT]Relation.Binary.Sigm..>20-Mar-2018 18:41 1.1K 
[TXT]Relation.Binary.Simp..>20-Mar-2018 18:41 7.5K 
[TXT]Relation.Binary.html 20-Mar-2018 18:41 95K 
[TXT]Relation.Nullary.Dec..>20-Mar-2018 18:41 38K 
[TXT]Relation.Nullary.Neg..>20-Mar-2018 18:41 69K 
[TXT]Relation.Nullary.Pro..>20-Mar-2018 18:41 5.3K 
[TXT]Relation.Nullary.Uni..>20-Mar-2018 18:41 66K 
[TXT]Relation.Nullary.html 20-Mar-2018 18:41 4.0K 
[TXT]Relation.Unary.html 20-Mar-2018 18:41 95K 
[TXT]SingletonChunks.html 20-Mar-2018 18:41 108K 
[TXT]Stream.Equality.html 20-Mar-2018 18:41 56K 
[TXT]Stream.Pointwise.html 20-Mar-2018 18:41 76K 
[TXT]Stream.Programs.html 20-Mar-2018 18:41 32K 
[TXT]Stream.html 20-Mar-2018 18:41 1.0K 
[TXT]StreamProg.html 20-Mar-2018 18:41 67K 
[TXT]Strict.html 20-Mar-2018 18:41 6.7K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 36K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 86K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 48K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 31K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 153K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 16K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 129K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 55K 
[TXT]StructurallyRecursiv..>20-Mar-2018 18:41 3.2K 
[TXT]ThueMorse.html 20-Mar-2018 18:41 199K 
[TXT]ThueMorseLeq.html 20-Mar-2018 18:41 78K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 24K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 52K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 54K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 29K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 216K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 108K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 20K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 40K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 49K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 42K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 107K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 3.0K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 20K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 25K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 134K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 57K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 152K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 40K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 151K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 113K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 52K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 137K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 49K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 55K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 232K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 48K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 33K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 65K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 77K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 12K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 27K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 111K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 87K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 227K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 11K 
[TXT]TotalParserCombinato..>20-Mar-2018 18:41 7.6K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 15K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 180K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 186K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 71K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 39K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 67K 
[TXT]TotalRecognisers.Lef..>20-Mar-2018 18:41 242K 
[TXT]TotalRecognisers.Sim..>20-Mar-2018 18:41 52K 
[TXT]TotalRecognisers.Sim..>20-Mar-2018 18:41 12K 
[TXT]TotalRecognisers.Sim..>20-Mar-2018 18:41 31K 
[TXT]TotalRecognisers.Sim..>20-Mar-2018 18:41 104K 
[TXT]TotalRecognisers.html 20-Mar-2018 18:41 5.0K 
[TXT]Tree.html 20-Mar-2018 18:41 19K 
[TXT]UniverseIndex.html 20-Mar-2018 18:41 22K 
[TXT]VenanziosProblem.html 20-Mar-2018 18:41 77K 

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