Index of /~nad/listings/codata

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory   -  
[TXT]AdmissibleButNotPost..>2023-09-29 17:41 158K 
[TXT]Agda.Builtin.Bool.html 2023-09-29 17:41 3.1K 
[TXT]Agda.Builtin.Char.Pr..>2023-09-29 17:41 2.1K 
[TXT]Agda.Builtin.Char.html 2023-09-29 17:41 4.0K 
[TXT]Agda.Builtin.Coinduc..>2023-09-29 17:41 4.2K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:41 2.3K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:41 2.6K 
[TXT]Agda.Builtin.IO.html 2023-09-29 17:41 2.4K 
[TXT]Agda.Builtin.List.html 2023-09-29 17:41 4.7K 
[TXT]Agda.Builtin.Maybe.html2023-09-29 17:41 2.3K 
[TXT]Agda.Builtin.Nat.html 2023-09-29 17:41 23K 
[TXT]Agda.Builtin.Sigma.html2023-09-29 17:41 3.4K 
[TXT]Agda.Builtin.Strict...>2023-09-29 17:41 4.8K 
[TXT]Agda.Builtin.String...>2023-09-29 17:41 3.2K 
[TXT]Agda.Builtin.String...>2023-09-29 17:41 10K 
[TXT]Agda.Builtin.Unit.html 2023-09-29 17:41 1.7K 
[TXT]Agda.Primitive.html 2023-09-29 17:41 5.4K 
[TXT]Agda.css 2023-09-29 17:41 1.8K 
[TXT]Algebra.Bundles.Raw...>2023-09-29 17:41 54K 
[TXT]Algebra.Bundles.html 2023-09-29 17:41 255K 
[TXT]Algebra.Consequences..>2023-09-29 17:41 7.1K 
[TXT]Algebra.Consequences..>2023-09-29 17:41 39K 
[TXT]Algebra.Consequences..>2023-09-29 17:41 165K 
[TXT]Algebra.Construct.Li..>2023-09-29 17:41 83K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:41 17K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:41 7.3K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:41 18K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:41 13K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:41 57K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:41 109K 
[TXT]Algebra.Core.html 2023-09-29 17:41 3.3K 
[TXT]Algebra.Definitions...>2023-09-29 17:41 16K 
[TXT]Algebra.Definitions...>2023-09-29 17:41 11K 
[TXT]Algebra.Definitions...>2023-09-29 17:41 21K 
[TXT]Algebra.Definitions...>2023-09-29 17:41 118K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:41 7.2K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:41 51K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:41 4.5K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:41 18K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:41 6.3K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:41 293K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:41 6.0K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:41 42K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:41 11K 
[TXT]Algebra.Lattice.Stru..>2023-09-29 17:41 28K 
[TXT]Algebra.Lattice.Stru..>2023-09-29 17:41 41K 
[TXT]Algebra.Lattice.html 2023-09-29 17:41 1.9K 
[TXT]Algebra.Morphism.Def..>2023-09-29 17:41 11K 
[TXT]Algebra.Morphism.Str..>2023-09-29 17:41 177K 
[TXT]Algebra.Morphism.html 2023-09-29 17:41 47K 
[TXT]Algebra.Properties.A..>2023-09-29 17:41 12K 
[TXT]Algebra.Properties.C..>2023-09-29 17:41 112K 
[TXT]Algebra.Properties.G..>2023-09-29 17:41 52K 
[TXT]Algebra.Properties.M..>2023-09-29 17:41 30K 
[TXT]Algebra.Properties.R..>2023-09-29 17:41 41K 
[TXT]Algebra.Properties.S..>2023-09-29 17:41 8.2K 
[TXT]Algebra.Properties.S..>2023-09-29 17:41 38K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:41 43K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:41 96K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:41 4.3K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:41 294K 
[TXT]Algebra.Structures.B..>2023-09-29 17:41 64K 
[TXT]Algebra.Structures.html2023-09-29 17:41 210K 
[TXT]Algebra.html 2023-09-29 17:41 1.9K 
[TXT]ArbitraryChunks.html 2023-09-29 17:41 89K 
[TXT]Axiom.ExcludedMiddle..>2023-09-29 17:41 2.9K 
[TXT]Axiom.Extensionality..>2023-09-29 17:41 11K 
[TXT]Axiom.Extensionality..>2023-09-29 17:41 21K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:41 2.6K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:41 23K 
[TXT]BreadthFirst.Lemmas...>2023-09-29 17:41 174K 
[TXT]BreadthFirst.Program..>2023-09-29 17:41 58K 
[TXT]BreadthFirst.Univers..>2023-09-29 17:41 31K 
[TXT]BreadthFirst.html 2023-09-29 17:41 53K 
[TXT]BreadthFirstWithoutP..>2023-09-29 17:41 46K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 31K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 20K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 7.5K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 10K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 7.7K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 115K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 11K 
[TXT]Codata.Musical.Colis..>2023-09-29 17:41 93K 
[TXT]Codata.Musical.Conat..>2023-09-29 17:41 8.5K 
[TXT]Codata.Musical.Conat..>2023-09-29 17:41 20K 
[TXT]Codata.Musical.Costr..>2023-09-29 17:41 3.6K 
[TXT]Codata.Musical.Notat..>2023-09-29 17:41 1.1K 
[TXT]Codata.Musical.Strea..>2023-09-29 17:41 65K 
[TXT]Contractive.Examples..>2023-09-29 17:41 53K 
[TXT]Contractive.Function..>2023-09-29 17:41 20K 
[TXT]Contractive.Stream.html2023-09-29 17:41 46K 
[TXT]Contractive.html 2023-09-29 17:41 58K 
[TXT]Data.Bool.Base.html 2023-09-29 17:41 13K 
[TXT]Data.Bool.Properties..>2023-09-29 17:41 204K 
[TXT]Data.Bool.Show.html 2023-09-29 17:41 2.5K 
[TXT]Data.Bool.html 2023-09-29 17:41 2.9K 
[TXT]Data.Char.Base.html 2023-09-29 17:41 11K 
[TXT]Data.Char.Properties..>2023-09-29 17:41 59K 
[TXT]Data.Char.html 2023-09-29 17:41 2.1K 
[TXT]Data.DifferenceList...>2023-09-29 17:41 20K 
[TXT]Data.Digit.html 2023-09-29 17:41 43K 
[TXT]Data.Empty.Irrelevan..>2023-09-29 17:41 2.2K 
[TXT]Data.Empty.Polymorph..>2023-09-29 17:41 3.8K 
[TXT]Data.Empty.html 2023-09-29 17:41 4.1K 
[TXT]Data.Fin.Base.html 2023-09-29 17:41 117K 
[TXT]Data.Fin.Patterns.html 2023-09-29 17:41 4.3K 
[TXT]Data.Fin.Properties...>2023-09-29 17:41 540K 
[TXT]Data.Fin.Substitutio..>2023-09-29 17:41 339K 
[TXT]Data.Fin.Substitutio..>2023-09-29 17:41 14K 
[TXT]Data.Fin.Substitutio..>2023-09-29 17:41 54K 
[TXT]Data.Fin.html 2023-09-29 17:41 4.5K 
[TXT]Data.Irrelevant.html 2023-09-29 17:41 12K 
[TXT]Data.List.Base.html 2023-09-29 17:41 194K 
[TXT]Data.List.Countdown...>2023-09-29 17:41 98K 
[TXT]Data.List.Effectful...>2023-09-29 17:41 142K 
[TXT]Data.List.Extrema.Co..>2023-09-29 17:41 60K 
[TXT]Data.List.Extrema.html 2023-09-29 17:41 132K 
[TXT]Data.List.Membership..>2023-09-29 17:41 4.6K 
[TXT]Data.List.Membership..>2023-09-29 17:41 6.2K 
[TXT]Data.List.Membership..>2023-09-29 17:41 36K 
[TXT]Data.List.Membership..>2023-09-29 17:41 202K 
[TXT]Data.List.Membership..>2023-09-29 17:41 9.3K 
[TXT]Data.List.Membership..>2023-09-29 17:41 227K 
[TXT]Data.List.Membership..>2023-09-29 17:41 19K 
[TXT]Data.List.NonEmpty.B..>2023-09-29 17:41 139K 
[TXT]Data.List.NonEmpty.E..>2023-09-29 17:41 23K 
[TXT]Data.List.NonEmpty.P..>2023-09-29 17:41 77K 
[TXT]Data.List.NonEmpty.R..>2023-09-29 17:41 10K 
[TXT]Data.List.NonEmpty.html2023-09-29 17:41 4.7K 
[TXT]Data.List.Properties..>2023-09-29 17:41 618K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 338K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 6.3K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 48K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 21K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 92K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 62K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 34K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 231K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 35K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 385K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 42K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 26K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 37K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 127K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 10K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 512K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 59K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 93K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 103K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 2.8K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 99K 
[TXT]Data.List.Relation.B..>2023-09-29 17:41 10K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 411K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 110K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 6.3K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 36K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 452K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 38K 
[TXT]Data.List.Relation.U..>2023-09-29 17:41 5.7K 
[TXT]Data.List.Reverse.html 2023-09-29 17:41 9.6K 
[TXT]Data.List.html 2023-09-29 17:41 1.3K 
[TXT]Data.Maybe.Base.html 2023-09-29 17:41 37K 
[TXT]Data.Maybe.Effectful..>2023-09-29 17:41 17K 
[TXT]Data.Maybe.Effectful..>2023-09-29 17:41 20K 
[TXT]Data.Maybe.Propertie..>2023-09-29 17:41 55K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:41 49K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:41 54K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:41 31K 
[TXT]Data.Maybe.html 2023-09-29 17:41 7.5K 
[TXT]Data.Nat.Base.html 2023-09-29 17:41 83K 
[TXT]Data.Nat.DivMod.Core..>2023-09-29 17:41 222K 
[TXT]Data.Nat.DivMod.html 2023-09-29 17:41 363K 
[TXT]Data.Nat.Divisibilit..>2023-09-29 17:41 15K 
[TXT]Data.Nat.Divisibilit..>2023-09-29 17:41 158K 
[TXT]Data.Nat.Induction.html2023-09-29 17:41 25K 
[TXT]Data.Nat.InfinitelyO..>2023-09-29 17:41 36K 
[TXT]Data.Nat.Properties...>2023-09-29 17:41 908K 
[TXT]Data.Nat.Show.html 2023-09-29 17:41 23K 
[TXT]Data.Nat.Solver.html 2023-09-29 17:41 2.4K 
[TXT]Data.Nat.html 2023-09-29 17:41 5.7K 
[TXT]Data.Parity.Base.html 2023-09-29 17:41 19K 
[TXT]Data.Product.Algebra..>2023-09-29 17:41 52K 
[TXT]Data.Product.Base.html 2023-09-29 17:41 87K 
[TXT]Data.Product.Functio..>2023-09-29 17:41 159K 
[TXT]Data.Product.Functio..>2023-09-29 17:41 36K 
[TXT]Data.Product.Functio..>2023-09-29 17:41 55K 
[TXT]Data.Product.Propert..>2023-09-29 17:41 55K 
[TXT]Data.Product.Relatio..>2023-09-29 17:41 113K 
[TXT]Data.Product.Relatio..>2023-09-29 17:41 5.4K 
[TXT]Data.Product.html 2023-09-29 17:41 9.0K 
[TXT]Data.Sign.Base.html 2023-09-29 17:41 8.9K 
[TXT]Data.String.Base.html 2023-09-29 17:41 45K 
[TXT]Data.String.Properti..>2023-09-29 17:41 33K 
[TXT]Data.String.html 2023-09-29 17:41 18K 
[TXT]Data.Sum.Algebra.html 2023-09-29 17:41 30K 
[TXT]Data.Sum.Base.html 2023-09-29 17:41 26K 
[TXT]Data.Sum.Function.Pr..>2023-09-29 17:41 34K 
[TXT]Data.Sum.Function.Se..>2023-09-29 17:41 56K 
[TXT]Data.Sum.Properties...>2023-09-29 17:41 60K 
[TXT]Data.Sum.Relation.Bi..>2023-09-29 17:41 111K 
[TXT]Data.Sum.Relation.Un..>2023-09-29 17:41 15K 
[TXT]Data.Sum.html 2023-09-29 17:41 17K 
[TXT]Data.These.Base.html 2023-09-29 17:41 36K 
[TXT]Data.Unit.Base.html 2023-09-29 17:41 1.9K 
[TXT]Data.Unit.NonEta.html 2023-09-29 17:41 7.1K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:41 3.3K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:41 23K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:41 1.9K 
[TXT]Data.Unit.Properties..>2023-09-29 17:41 16K 
[TXT]Data.Unit.html 2023-09-29 17:41 1.7K 
[TXT]Data.Vec.Base.html 2023-09-29 17:41 153K 
[TXT]Data.Vec.Bounded.Bas..>2023-09-29 17:41 68K 
[TXT]Data.Vec.Bounded.html 2023-09-29 17:41 14K 
[TXT]Data.Vec.Functional...>2023-09-29 17:41 69K 
[TXT]Data.Vec.N-ary.html 2023-09-29 17:41 92K 
[TXT]Data.Vec.Properties...>2023-09-29 17:41 694K 
[TXT]Data.Vec.Recursive.html2023-09-29 17:41 81K 
[TXT]Data.Vec.html 2023-09-29 17:41 12K 
[TXT]DataAndCodata.html 2023-09-29 17:41 22K 
[TXT]Effect.Applicative.I..>2023-09-29 17:41 45K 
[TXT]Effect.Applicative.html2023-09-29 17:41 36K 
[TXT]Effect.Choice.html 2023-09-29 17:41 4.4K 
[TXT]Effect.Comonad.html 2023-09-29 17:41 12K 
[TXT]Effect.Empty.html 2023-09-29 17:41 3.4K 
[TXT]Effect.Functor.html 2023-09-29 17:41 13K 
[TXT]Effect.Monad.Indexed..>2023-09-29 17:41 29K 
[TXT]Effect.Monad.Partial..>2023-09-29 17:41 87K 
[TXT]Effect.Monad.Partial..>2023-09-29 17:41 442K 
[TXT]Effect.Monad.State.I..>2023-09-29 17:41 37K 
[TXT]Effect.Monad.html 2023-09-29 17:41 32K 
[TXT]Function.Base.html 2023-09-29 17:41 75K 
[TXT]Function.Bijection.html2023-09-29 17:41 33K 
[TXT]Function.Bundles.html 2023-09-29 17:41 110K 
[TXT]Function.Consequence..>2023-09-29 17:41 22K 
[TXT]Function.Consequence..>2023-09-29 17:41 34K 
[TXT]Function.Construct.C..>2023-09-29 17:41 115K 
[TXT]Function.Construct.I..>2023-09-29 17:41 45K 
[TXT]Function.Construct.S..>2023-09-29 17:41 72K 
[TXT]Function.Core.html 2023-09-29 17:41 5.0K 
[TXT]Function.Definitions..>2023-09-29 17:41 21K 
[TXT]Function.Equality.html 2023-09-29 17:41 40K 
[TXT]Function.Equivalence..>2023-09-29 17:41 40K 
[TXT]Function.HalfAdjoint..>2023-09-29 17:41 46K 
[TXT]Function.Identity.Ef..>2023-09-29 17:41 7.8K 
[TXT]Function.Injection.html2023-09-29 17:41 23K 
[TXT]Function.Inverse.html 2023-09-29 17:41 60K 
[TXT]Function.LeftInverse..>2023-09-29 17:41 42K 
[TXT]Function.Metric.Bund..>2023-09-29 17:41 37K 
[TXT]Function.Metric.Core..>2023-09-29 17:41 2.8K 
[TXT]Function.Metric.Defi..>2023-09-29 17:41 35K 
[TXT]Function.Metric.Nat...>2023-09-29 17:41 28K 
[TXT]Function.Metric.Nat...>2023-09-29 17:41 2.6K 
[TXT]Function.Metric.Nat...>2023-09-29 17:41 17K 
[TXT]Function.Metric.Nat...>2023-09-29 17:41 18K 
[TXT]Function.Metric.Nat...>2023-09-29 17:41 1.8K 
[TXT]Function.Metric.Stru..>2023-09-29 17:41 22K 
[TXT]Function.Properties...>2023-09-29 17:41 20K 
[TXT]Function.Properties...>2023-09-29 17:41 12K 
[TXT]Function.Properties...>2023-09-29 17:41 28K 
[TXT]Function.Properties...>2023-09-29 17:41 7.7K 
[TXT]Function.Properties...>2023-09-29 17:41 13K 
[TXT]Function.Related.Pro..>2023-09-29 17:41 126K 
[TXT]Function.Related.Typ..>2023-09-29 17:41 185K 
[TXT]Function.Related.html 2023-09-29 17:41 163K 
[TXT]Function.Strict.html 2023-09-29 17:41 15K 
[TXT]Function.Structures...>2023-09-29 17:41 43K 
[TXT]Function.Surjection...>2023-09-29 17:41 33K 
[TXT]Function.html 2023-09-29 17:41 2.0K 
[TXT]Hinze.Lemmas.html 2023-09-29 17:41 48K 
[TXT]Hinze.Section2-4.html 2023-09-29 17:41 74K 
[TXT]Hinze.Section3.html 2023-09-29 17:41 64K 
[TXT]Hinze.Simplified.Sec..>2023-09-29 17:41 63K 
[TXT]Hinze.Simplified.Sec..>2023-09-29 17:41 52K 
[TXT]IO.Base.html 2023-09-29 17:41 42K 
[TXT]IO.Finite.html 2023-09-29 17:41 8.7K 
[TXT]IO.Infinite.html 2023-09-29 17:41 8.0K 
[TXT]IO.Primitive.Finite...>2023-09-29 17:41 11K 
[TXT]IO.Primitive.Infinit..>2023-09-29 17:41 13K 
[TXT]IO.Primitive.html 2023-09-29 17:41 6.1K 
[TXT]IO.html 2023-09-29 17:41 24K 
[TXT]Induction.WellFounde..>2023-09-29 17:41 87K 
[TXT]Induction.html 2023-09-29 17:41 17K 
[TXT]InductiveStreamEqual..>2023-09-29 17:41 43K 
[TXT]InfinitelyOften.html 2023-09-29 17:41 237K 
[TXT]Lambda.Closure.Equiv..>2023-09-29 17:41 179K 
[TXT]Lambda.Closure.Equiv..>2023-09-29 17:41 145K 
[TXT]Lambda.Closure.Funct..>2023-09-29 17:41 281K 
[TXT]Lambda.Closure.Funct..>2023-09-29 17:41 123K 
[TXT]Lambda.Closure.Funct..>2023-09-29 17:41 303K 
[TXT]Lambda.Closure.Funct..>2023-09-29 17:41 414K 
[TXT]Lambda.Closure.Funct..>2023-09-29 17:41 42K 
[TXT]Lambda.Closure.Funct..>2023-09-29 17:41 187K 
[TXT]Lambda.Closure.Relat..>2023-09-29 17:41 93K 
[TXT]Lambda.Substitution...>2023-09-29 17:41 17K 
[TXT]Lambda.Substitution...>2023-09-29 17:41 51K 
[TXT]Lambda.Substitution...>2023-09-29 17:41 15K 
[TXT]Lambda.Substitution...>2023-09-29 17:41 13K 
[TXT]Lambda.Substitution...>2023-09-29 17:41 96K 
[TXT]Lambda.Syntax.html 2023-09-29 17:41 35K 
[TXT]Lambda.VirtualMachin..>2023-09-29 17:41 215K 
[TXT]Lambda.html 2023-09-29 17:41 8.9K 
[TXT]LargeCombinators.html 2023-09-29 17:41 33K 
[TXT]Level.html 2023-09-29 17:41 5.6K 
[TXT]MapIterate.html 2023-09-29 17:41 56K 
[TXT]Mixfix.Acyclic.Examp..>2023-09-29 17:41 51K 
[TXT]Mixfix.Acyclic.Gramm..>2023-09-29 17:41 30K 
[TXT]Mixfix.Acyclic.Lemma..>2023-09-29 17:41 13K 
[TXT]Mixfix.Acyclic.Lib.html2023-09-29 17:41 206K 
[TXT]Mixfix.Acyclic.Prece..>2023-09-29 17:41 8.8K 
[TXT]Mixfix.Acyclic.Show...>2023-09-29 17:41 83K 
[TXT]Mixfix.Cyclic.Exampl..>2023-09-29 17:41 52K 
[TXT]Mixfix.Cyclic.Gramma..>2023-09-29 17:41 30K 
[TXT]Mixfix.Cyclic.Lib.html 2023-09-29 17:41 187K 
[TXT]Mixfix.Cyclic.Preced..>2023-09-29 17:41 8.4K 
[TXT]Mixfix.Cyclic.Show.html2023-09-29 17:41 66K 
[TXT]Mixfix.Cyclic.Unique..>2023-09-29 17:41 155K 
[TXT]Mixfix.Equivalence.html2023-09-29 17:41 110K 
[TXT]Mixfix.Expr.html 2023-09-29 17:41 35K 
[TXT]Mixfix.Fixity.html 2023-09-29 17:41 18K 
[TXT]Mixfix.Operator.html 2023-09-29 17:41 9.7K 
[TXT]Mixfix.html 2023-09-29 17:41 8.3K 
[TXT]MuNu.html 2023-09-29 17:41 36K 
[TXT]Nested.html 2023-09-29 17:41 97K 
[TXT]Operational-semantic..>2023-09-29 17:41 8.5K 
[TXT]RecursiveTypes.Seman..>2023-09-29 17:41 6.7K 
[TXT]RecursiveTypes.Subst..>2023-09-29 17:41 66K 
[TXT]RecursiveTypes.Subte..>2023-09-29 17:41 58K 
[TXT]RecursiveTypes.Subte..>2023-09-29 17:41 191K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 80K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 83K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 154K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 5.0K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 89K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 51K 
[TXT]RecursiveTypes.Subty..>2023-09-29 17:41 26K 
[TXT]RecursiveTypes.Synta..>2023-09-29 17:41 15K 
[TXT]RecursiveTypes.Synta..>2023-09-29 17:41 51K 
[TXT]RecursiveTypes.html 2023-09-29 17:41 6.5K 
[TXT]Relation.Binary.Bund..>2023-09-29 17:41 66K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 101K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 8.5K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 68K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 23K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 86K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 79K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 3.8K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 12K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 72K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 13K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 78K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 77K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 69K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 83K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:41 10K 
[TXT]Relation.Binary.Core..>2023-09-29 17:41 19K 
[TXT]Relation.Binary.Defi..>2023-09-29 17:41 91K 
[TXT]Relation.Binary.Hete..>2023-09-29 17:41 8.0K 
[TXT]Relation.Binary.Hete..>2023-09-29 17:41 130K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 11K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 21K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 15K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 10K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 2.1K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:41 68K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:41 12K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:41 61K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:41 1.7K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:41 6.3K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:41 38K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 15K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 34K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 9.8K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 18K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 17K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 5.5K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 45K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 104K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 4.1K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:41 53K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:41 45K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:41 20K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:41 69K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:41 6.5K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:41 3.5K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:41 7.4K 
[TXT]Relation.Binary.Refl..>2023-09-29 17:41 37K 
[TXT]Relation.Binary.Stru..>2023-09-29 17:41 62K 
[TXT]Relation.Binary.html 2023-09-29 17:41 1.9K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:41 56K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:41 32K 
[TXT]Relation.Nullary.Ind..>2023-09-29 17:41 3.2K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:41 21K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:41 38K 
[TXT]Relation.Nullary.Ref..>2023-09-29 17:41 34K 
[TXT]Relation.Nullary.Uni..>2023-09-29 17:41 68K 
[TXT]Relation.Nullary.html 2023-09-29 17:41 6.5K 
[TXT]Relation.Unary.Prope..>2023-09-29 17:41 113K 
[TXT]Relation.Unary.html 2023-09-29 17:41 91K 
[TXT]SingletonChunks.html 2023-09-29 17:41 109K 
[TXT]Stream.Equality.html 2023-09-29 17:41 56K 
[TXT]Stream.Pointwise.html 2023-09-29 17:41 76K 
[TXT]Stream.Programs.html 2023-09-29 17:41 32K 
[TXT]Stream.html 2023-09-29 17:41 1.0K 
[TXT]StreamProg.html 2023-09-29 17:41 67K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 38K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 93K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 49K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 31K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 154K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 17K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 129K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 56K 
[TXT]StructurallyRecursiv..>2023-09-29 17:41 3.2K 
[TXT]ThueMorse.html 2023-09-29 17:41 200K 
[TXT]ThueMorseLeq.html 2023-09-29 17:41 79K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 24K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 87K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 54K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 30K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 218K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 109K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 20K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 41K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 42K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 44K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 108K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 3.0K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 20K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 26K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 135K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 58K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 154K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 39K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 186K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 114K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 52K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 137K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 49K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 38K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 235K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 21K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 49K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 33K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 67K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 78K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 12K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 27K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 112K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 87K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 226K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 12K 
[TXT]TotalParserCombinato..>2023-09-29 17:41 7.8K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 15K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 182K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 185K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 72K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 39K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 67K 
[TXT]TotalRecognisers.Lef..>2023-09-29 17:41 250K 
[TXT]TotalRecognisers.Sim..>2023-09-29 17:41 52K 
[TXT]TotalRecognisers.Sim..>2023-09-29 17:41 12K 
[TXT]TotalRecognisers.Sim..>2023-09-29 17:41 32K 
[TXT]TotalRecognisers.Sim..>2023-09-29 17:41 104K 
[TXT]TotalRecognisers.html 2023-09-29 17:41 5.0K 
[TXT]Tree.html 2023-09-29 17:41 19K 
[TXT]UniverseIndex.html 2023-09-29 17:41 23K 
[TXT]VenanziosProblem.html 2023-09-29 17:41 78K 

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