Index of /~nad/listings/up-to

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory   -  
[TXT]Accessibility.html 2023-09-29 17:40 94K 
[TXT]Agda.Builtin.Bool.html 2023-09-29 17:40 3.1K 
[TXT]Agda.Builtin.Char.html 2023-09-29 17:40 4.0K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:40 2.6K 
[TXT]Agda.Builtin.Int.html 2023-09-29 17:40 3.4K 
[TXT]Agda.Builtin.List.html 2023-09-29 17:40 4.7K 
[TXT]Agda.Builtin.Maybe.html2023-09-29 17:40 2.3K 
[TXT]Agda.Builtin.Nat.html 2023-09-29 17:40 23K 
[TXT]Agda.Builtin.Sigma.html2023-09-29 17:40 3.4K 
[TXT]Agda.Builtin.Size.html 2023-09-29 17:40 4.2K 
[TXT]Agda.Builtin.String...>2023-09-29 17:40 10K 
[TXT]Agda.Builtin.Unit.html 2023-09-29 17:40 1.7K 
[TXT]Agda.Primitive.html 2023-09-29 17:40 5.4K 
[TXT]Agda.css 2023-09-29 17:40 1.8K 
[TXT]Algebra.Bundles.Raw...>2023-09-29 17:40 54K 
[TXT]Algebra.Bundles.html 2023-09-29 17:40 255K 
[TXT]Algebra.Consequences..>2023-09-29 17:40 7.1K 
[TXT]Algebra.Consequences..>2023-09-29 17:40 39K 
[TXT]Algebra.Consequences..>2023-09-29 17:40 165K 
[TXT]Algebra.Construct.Li..>2023-09-29 17:40 83K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:40 17K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:40 7.3K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:40 18K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:40 13K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:40 57K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:40 109K 
[TXT]Algebra.Core.html 2023-09-29 17:40 3.3K 
[TXT]Algebra.Definitions...>2023-09-29 17:40 16K 
[TXT]Algebra.Definitions...>2023-09-29 17:40 11K 
[TXT]Algebra.Definitions...>2023-09-29 17:40 21K 
[TXT]Algebra.Definitions...>2023-09-29 17:40 118K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:40 7.2K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:40 51K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:40 4.5K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:40 18K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:40 6.3K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:40 293K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:40 6.0K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:40 42K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:40 11K 
[TXT]Algebra.Lattice.Stru..>2023-09-29 17:40 41K 
[TXT]Algebra.Morphism.Def..>2023-09-29 17:40 11K 
[TXT]Algebra.Morphism.Str..>2023-09-29 17:40 177K 
[TXT]Algebra.Morphism.html 2023-09-29 17:40 47K 
[TXT]Algebra.Properties.A..>2023-09-29 17:40 12K 
[TXT]Algebra.Properties.C..>2023-09-29 17:40 112K 
[TXT]Algebra.Properties.G..>2023-09-29 17:40 52K 
[TXT]Algebra.Properties.M..>2023-09-29 17:40 30K 
[TXT]Algebra.Properties.R..>2023-09-29 17:40 41K 
[TXT]Algebra.Properties.S..>2023-09-29 17:40 8.2K 
[TXT]Algebra.Properties.S..>2023-09-29 17:40 38K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:40 43K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:40 96K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:40 4.3K 
[TXT]Algebra.Solver.Ring...>2023-09-29 17:40 294K 
[TXT]Algebra.Structures.B..>2023-09-29 17:40 64K 
[TXT]Algebra.Structures.html2023-09-29 17:40 210K 
[TXT]Algebra.html 2023-09-29 17:40 1.9K 
[TXT]Axiom.Extensionality..>2023-09-29 17:40 21K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:40 23K 
[TXT]Bijection.html 2023-09-29 17:40 226K 
[TXT]Bisimilarity.6-2-5.html2023-09-29 17:40 94K 
[TXT]Bisimilarity.CCS.Cla..>2023-09-29 17:40 96K 
[TXT]Bisimilarity.CCS.Exa..>2023-09-29 17:40 61K 
[TXT]Bisimilarity.CCS.Exa..>2023-09-29 17:40 62K 
[TXT]Bisimilarity.CCS.Exa..>2023-09-29 17:40 464K 
[TXT]Bisimilarity.CCS.Gen..>2023-09-29 17:40 86K 
[TXT]Bisimilarity.CCS.html 2023-09-29 17:40 363K 
[TXT]Bisimilarity.Classic..>2023-09-29 17:40 5.0K 
[TXT]Bisimilarity.Classic..>2023-09-29 17:40 132K 
[TXT]Bisimilarity.Compari..>2023-09-29 17:40 79K 
[TXT]Bisimilarity.Delay-m..>2023-09-29 17:40 21K 
[TXT]Bisimilarity.Equatio..>2023-09-29 17:40 19K 
[TXT]Bisimilarity.General..>2023-09-29 17:40 108K 
[TXT]Bisimilarity.Step.html 2023-09-29 17:40 68K 
[TXT]Bisimilarity.Up-to.C..>2023-09-29 17:40 115K 
[TXT]Bisimilarity.Up-to.C..>2023-09-29 17:40 311K 
[TXT]Bisimilarity.Up-to.html2023-09-29 17:40 22K 
[TXT]Bisimilarity.Weak.Al..>2023-09-29 17:40 4.2K 
[TXT]Bisimilarity.Weak.Al..>2023-09-29 17:40 47K 
[TXT]Bisimilarity.Weak.Al..>2023-09-29 17:40 14K 
[TXT]Bisimilarity.Weak.Al..>2023-09-29 17:40 30K 
[TXT]Bisimilarity.Weak.Al..>2023-09-29 17:40 19K 
[TXT]Bisimilarity.Weak.CC..>2023-09-29 17:40 292K 
[TXT]Bisimilarity.Weak.CC..>2023-09-29 17:40 198K 
[TXT]Bisimilarity.Weak.De..>2023-09-29 17:40 157K 
[TXT]Bisimilarity.Weak.Eq..>2023-09-29 17:40 85K 
[TXT]Bisimilarity.Weak.Eq..>2023-09-29 17:40 23K 
[TXT]Bisimilarity.Weak.Up..>2023-09-29 17:40 67K 
[TXT]Bisimilarity.Weak.Up..>2023-09-29 17:40 96K 
[TXT]Bisimilarity.Weak.html 2023-09-29 17:40 92K 
[TXT]Bisimilarity.html 2023-09-29 17:40 55K 
[TXT]Bool.html 2023-09-29 17:40 74K 
[TXT]Conat.html 2023-09-29 17:40 432K 
[TXT]Data.Bool.Base.html 2023-09-29 17:40 13K 
[TXT]Data.Bool.Properties..>2023-09-29 17:40 204K 
[TXT]Data.Empty.Irrelevan..>2023-09-29 17:40 2.2K 
[TXT]Data.Empty.Polymorph..>2023-09-29 17:40 3.8K 
[TXT]Data.Empty.html 2023-09-29 17:40 4.1K 
[TXT]Data.Fin.Base.html 2023-09-29 17:40 117K 
[TXT]Data.Fin.Patterns.html 2023-09-29 17:40 4.3K 
[TXT]Data.Fin.Properties...>2023-09-29 17:40 540K 
[TXT]Data.Irrelevant.html 2023-09-29 17:40 12K 
[TXT]Data.List.Base.html 2023-09-29 17:40 194K 
[TXT]Data.List.Effectful...>2023-09-29 17:40 142K 
[TXT]Data.List.Extrema.Co..>2023-09-29 17:40 60K 
[TXT]Data.List.Extrema.html 2023-09-29 17:40 132K 
[TXT]Data.List.Membership..>2023-09-29 17:40 36K 
[TXT]Data.List.Membership..>2023-09-29 17:40 202K 
[TXT]Data.List.Membership..>2023-09-29 17:40 9.3K 
[TXT]Data.List.Membership..>2023-09-29 17:40 227K 
[TXT]Data.List.Membership..>2023-09-29 17:40 19K 
[TXT]Data.List.Properties..>2023-09-29 17:40 618K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 6.3K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 48K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 26K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 37K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 127K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 2.8K 
[TXT]Data.List.Relation.B..>2023-09-29 17:40 10K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 411K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 110K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 6.3K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 36K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 452K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 38K 
[TXT]Data.List.Relation.U..>2023-09-29 17:40 5.7K 
[TXT]Data.Maybe.Base.html 2023-09-29 17:40 37K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:40 54K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:40 31K 
[TXT]Data.Nat.Base.html 2023-09-29 17:40 83K 
[TXT]Data.Nat.DivMod.Core..>2023-09-29 17:40 222K 
[TXT]Data.Nat.DivMod.html 2023-09-29 17:40 363K 
[TXT]Data.Nat.Divisibilit..>2023-09-29 17:40 15K 
[TXT]Data.Nat.Divisibilit..>2023-09-29 17:40 158K 
[TXT]Data.Nat.Induction.html2023-09-29 17:40 25K 
[TXT]Data.Nat.Properties...>2023-09-29 17:40 908K 
[TXT]Data.Nat.Solver.html 2023-09-29 17:40 2.4K 
[TXT]Data.Nat.html 2023-09-29 17:40 5.7K 
[TXT]Data.Parity.Base.html 2023-09-29 17:40 19K 
[TXT]Data.Product.Algebra..>2023-09-29 17:40 52K 
[TXT]Data.Product.Base.html 2023-09-29 17:40 87K 
[TXT]Data.Product.Functio..>2023-09-29 17:40 159K 
[TXT]Data.Product.Functio..>2023-09-29 17:40 36K 
[TXT]Data.Product.Functio..>2023-09-29 17:40 55K 
[TXT]Data.Product.Propert..>2023-09-29 17:40 55K 
[TXT]Data.Product.Relatio..>2023-09-29 17:40 113K 
[TXT]Data.Product.Relatio..>2023-09-29 17:40 5.4K 
[TXT]Data.Sign.Base.html 2023-09-29 17:40 8.9K 
[TXT]Data.Sum.Algebra.html 2023-09-29 17:40 30K 
[TXT]Data.Sum.Base.html 2023-09-29 17:40 26K 
[TXT]Data.Sum.Function.Pr..>2023-09-29 17:40 34K 
[TXT]Data.Sum.Function.Se..>2023-09-29 17:40 56K 
[TXT]Data.Sum.Properties...>2023-09-29 17:40 60K 
[TXT]Data.Sum.Relation.Bi..>2023-09-29 17:40 111K 
[TXT]Data.These.Base.html 2023-09-29 17:40 36K 
[TXT]Data.Unit.Base.html 2023-09-29 17:40 1.9K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:40 3.3K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:40 23K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:40 1.9K 
[TXT]Data.Unit.Properties..>2023-09-29 17:40 16K 
[TXT]Data.Unit.html 2023-09-29 17:40 1.7K 
[TXT]Data.Vec.Base.html 2023-09-29 17:40 153K 
[TXT]Data.Vec.Bounded.Bas..>2023-09-29 17:40 68K 
[TXT]Data.Vec.Functional...>2023-09-29 17:40 69K 
[TXT]Data.Vec.N-ary.html 2023-09-29 17:40 92K 
[TXT]Data.Vec.html 2023-09-29 17:40 12K 
[TXT]Delay-monad.Bisimila..>2023-09-29 17:40 57K 
[TXT]Delay-monad.Bisimila..>2023-09-29 17:40 9.0K 
[TXT]Delay-monad.Bisimila..>2023-09-29 17:40 195K 
[TXT]Delay-monad.Bisimila..>2023-09-29 17:40 246K 
[TXT]Delay-monad.Partial-..>2023-09-29 17:40 158K 
[TXT]Delay-monad.Terminat..>2023-09-29 17:40 42K 
[TXT]Delay-monad.html 2023-09-29 17:40 16K 
[TXT]Double-negation.html 2023-09-29 17:40 96K 
[TXT]Effect.Applicative.html2023-09-29 17:40 36K 
[TXT]Effect.Choice.html 2023-09-29 17:40 4.4K 
[TXT]Effect.Empty.html 2023-09-29 17:40 3.4K 
[TXT]Effect.Functor.html 2023-09-29 17:40 13K 
[TXT]Effect.Monad.html 2023-09-29 17:40 32K 
[TXT]Embedding.html 2023-09-29 17:40 82K 
[TXT]Equality.Decidable-U..>2023-09-29 17:40 76K 
[TXT]Equality.Decision-pr..>2023-09-29 17:40 97K 
[TXT]Equality.Groupoid.html 2023-09-29 17:40 100K 
[TXT]Equality.Instances-r..>2023-09-29 17:40 120K 
[TXT]Equality.Proposition..>2023-09-29 17:40 19K 
[TXT]Equality.Tactic.html 2023-09-29 17:40 129K 
[TXT]Equality.html 2023-09-29 17:40 1.0M 
[TXT]Equational-reasoning..>2023-09-29 17:40 73K 
[TXT]Equivalence-relation..>2023-09-29 17:40 82K 
[TXT]Equivalence.Contract..>2023-09-29 17:40 128K 
[TXT]Equivalence.Erased.B..>2023-09-29 17:40 97K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:40 70K 
[TXT]Equivalence.Half-adj..>2023-09-29 17:40 133K 
[TXT]Equivalence.List.html 2023-09-29 17:40 355K 
[TXT]Equivalence.Path-spl..>2023-09-29 17:40 413K 
[TXT]Equivalence.html 2023-09-29 17:40 502K 
[TXT]Erased.Basics.html 2023-09-29 17:40 14K 
[TXT]Erased.Box-cong-axio..>2023-09-29 17:40 7.0K 
[TXT]Erased.Level-1.html 2023-09-29 17:40 1.0M 
[TXT]Excluded-middle.html 2023-09-29 17:40 6.6K 
[TXT]Expansion.CCS.html 2023-09-29 17:40 339K 
[TXT]Expansion.Delay-mona..>2023-09-29 17:40 85K 
[TXT]Expansion.Equational..>2023-09-29 17:40 44K 
[TXT]Expansion.html 2023-09-29 17:40 103K 
[TXT]Extensionality.html 2023-09-29 17:40 189K 
[TXT]Fin.html 2023-09-29 17:40 182K 
[TXT]For-iterated-equalit..>2023-09-29 17:40 337K 
[TXT]Function-universe.Si..>2023-09-29 17:40 28K 
[TXT]Function-universe.html 2023-09-29 17:40 2.5M 
[TXT]Function.Base.html 2023-09-29 17:40 75K 
[TXT]Function.Bijection.html2023-09-29 17:40 33K 
[TXT]Function.Bundles.html 2023-09-29 17:40 110K 
[TXT]Function.Consequence..>2023-09-29 17:40 22K 
[TXT]Function.Consequence..>2023-09-29 17:40 34K 
[TXT]Function.Construct.C..>2023-09-29 17:40 115K 
[TXT]Function.Construct.I..>2023-09-29 17:40 45K 
[TXT]Function.Construct.S..>2023-09-29 17:40 72K 
[TXT]Function.Core.html 2023-09-29 17:40 5.0K 
[TXT]Function.Definitions..>2023-09-29 17:40 21K 
[TXT]Function.Equality.html 2023-09-29 17:40 40K 
[TXT]Function.Equivalence..>2023-09-29 17:40 40K 
[TXT]Function.HalfAdjoint..>2023-09-29 17:40 46K 
[TXT]Function.Injection.html2023-09-29 17:40 23K 
[TXT]Function.Inverse.html 2023-09-29 17:40 60K 
[TXT]Function.LeftInverse..>2023-09-29 17:40 42K 
[TXT]Function.Metric.Bund..>2023-09-29 17:40 37K 
[TXT]Function.Metric.Core..>2023-09-29 17:40 2.8K 
[TXT]Function.Metric.Defi..>2023-09-29 17:40 35K 
[TXT]Function.Metric.Nat...>2023-09-29 17:40 28K 
[TXT]Function.Metric.Nat...>2023-09-29 17:40 2.6K 
[TXT]Function.Metric.Nat...>2023-09-29 17:40 17K 
[TXT]Function.Metric.Nat...>2023-09-29 17:40 18K 
[TXT]Function.Metric.Nat...>2023-09-29 17:40 1.8K 
[TXT]Function.Metric.Stru..>2023-09-29 17:40 22K 
[TXT]Function.Properties...>2023-09-29 17:40 20K 
[TXT]Function.Properties...>2023-09-29 17:40 28K 
[TXT]Function.Properties...>2023-09-29 17:40 7.7K 
[TXT]Function.Properties...>2023-09-29 17:40 13K 
[TXT]Function.Related.Pro..>2023-09-29 17:40 126K 
[TXT]Function.Related.Typ..>2023-09-29 17:40 185K 
[TXT]Function.Related.html 2023-09-29 17:40 163K 
[TXT]Function.Structures...>2023-09-29 17:40 43K 
[TXT]Function.Surjection...>2023-09-29 17:40 33K 
[TXT]Groupoid.html 2023-09-29 17:40 189K 
[TXT]H-level.Closure.html 2023-09-29 17:40 406K 
[TXT]H-level.html 2023-09-29 17:40 53K 
[TXT]Indexed-container.Co..>2023-09-29 17:40 593K 
[TXT]Indexed-container.De..>2023-09-29 17:40 62K 
[TXT]Indexed-container.html 2023-09-29 17:40 265K 
[TXT]Induction.WellFounde..>2023-09-29 17:40 87K 
[TXT]Induction.html 2023-09-29 17:40 17K 
[TXT]Injection.html 2023-09-29 17:40 18K 
[TXT]Integer.Basics.html 2023-09-29 17:40 40K 
[TXT]Labelled-transition-..>2023-09-29 17:40 17K 
[TXT]Labelled-transition-..>2023-09-29 17:40 352K 
[TXT]Labelled-transition-..>2023-09-29 17:40 119K 
[TXT]Labelled-transition-..>2023-09-29 17:40 104K 
[TXT]Labelled-transition-..>2023-09-29 17:40 238K 
[TXT]Level.html 2023-09-29 17:40 5.6K 
[TXT]List.html 2023-09-29 17:40 265K 
[TXT]Logical-equivalence...>2023-09-29 17:40 50K 
[TXT]Modality.Basics.html 2023-09-29 17:40 2.1M 
[TXT]Monad.Raw.html 2023-09-29 17:40 18K 
[TXT]Monad.html 2023-09-29 17:40 115K 
[TXT]Nat.Solver.html 2023-09-29 17:40 59K 
[TXT]Nat.html 2023-09-29 17:40 476K 
[TXT]Pointed-type.html 2023-09-29 17:40 197K 
[TXT]Preimage.html 2023-09-29 17:40 59K 
[TXT]Prelude.Size.html 2023-09-29 17:40 3.1K 
[TXT]Prelude.html 2023-09-29 17:40 123K 
[TXT]Pullback.html 2023-09-29 17:40 102K 
[TXT]Relation.Binary.Bund..>2023-09-29 17:40 66K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:40 101K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:40 72K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:40 78K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:40 77K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:40 69K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:40 83K 
[TXT]Relation.Binary.Core..>2023-09-29 17:40 19K 
[TXT]Relation.Binary.Defi..>2023-09-29 17:40 91K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:40 11K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:40 15K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:40 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:40 10K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:40 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:40 2.1K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:40 68K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:40 12K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:40 61K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:40 1.7K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:40 6.3K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:40 38K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 15K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 34K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 9.8K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 18K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 17K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 5.5K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 45K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 104K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:40 53K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:40 45K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:40 20K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:40 69K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:40 3.5K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:40 7.4K 
[TXT]Relation.Binary.Refl..>2023-09-29 17:40 37K 
[TXT]Relation.Binary.Stru..>2023-09-29 17:40 62K 
[TXT]Relation.Binary.html 2023-09-29 17:40 1.9K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:40 56K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:40 32K 
[TXT]Relation.Nullary.Ind..>2023-09-29 17:40 3.2K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:40 21K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:40 38K 
[TXT]Relation.Nullary.Ref..>2023-09-29 17:40 34K 
[TXT]Relation.Nullary.html 2023-09-29 17:40 6.5K 
[TXT]Relation.Unary.Prope..>2023-09-29 17:40 113K 
[TXT]Relation.Unary.html 2023-09-29 17:40 91K 
[TXT]Relation.html 2023-09-29 17:40 218K 
[TXT]Similarity.CCS.html 2023-09-29 17:40 133K 
[TXT]Similarity.Equationa..>2023-09-29 17:40 25K 
[TXT]Similarity.General.html2023-09-29 17:40 46K 
[TXT]Similarity.Step.html 2023-09-29 17:40 332K 
[TXT]Similarity.Weak.Equa..>2023-09-29 17:40 48K 
[TXT]Similarity.Weak.Up-t..>2023-09-29 17:40 10K 
[TXT]Similarity.Weak.html 2023-09-29 17:40 49K 
[TXT]Similarity.html 2023-09-29 17:40 29K 
[TXT]Surjection.html 2023-09-29 17:40 88K 
[TXT]Univalence-axiom.html 2023-09-29 17:40 706K 
[TXT]Up-to.Closure.html 2023-09-29 17:40 110K 
[TXT]Up-to.Via.html 2023-09-29 17:40 83K 
[TXT]Up-to.html 2023-09-29 17:40 300K 
[TXT]Vec.Dependent.html 2023-09-29 17:40 47K 

README
------------------------------------------------------------------------
-- Code related to the paper "Up-to Techniques using Sized Types"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module README where

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Some preliminaries

-- Overloaded "equational" reasoning combinators.

import Equational-reasoning

-- Unary and binary relations.

import Relation

------------------------------------------------------------------------
-- Containers

-- Indexed containers.

import Indexed-container

-- Container combinators.

import Indexed-container.Combinators

-- The delay monad defined as the greatest fixpoint of an indexed
-- container.

import Indexed-container.Delay-monad

------------------------------------------------------------------------
-- Up-to techniques

-- Up-to techniques, compatibility, size-preserving functions, and the
-- companion.

import Up-to

-- Closure properties for Compatible and Size-preserving.
--
-- (Some negative results in this module depend on code presented
-- further down.)

import Up-to.Closure

-- Up-to techniques via.

import Up-to.Via

------------------------------------------------------------------------
-- Labelled transition systems

-- Labelled transition systems (LTSs).

import Labelled-transition-system
import Labelled-transition-system.Equational-reasoning-instances

-- CCS.

import Labelled-transition-system.CCS

-- A labelled transition system for the delay monad.

import Labelled-transition-system.Delay-monad

-- An LTS from Section 6.2.5 of "Enhancements of the bisimulation
-- proof method" by Pous and Sangiorgi.

import Labelled-transition-system.6-2-5

------------------------------------------------------------------------
-- Similarity

-- The one-sided Step function, used to define similarity and the
-- two-sided Step function.

import Similarity.Step

-- A parametrised coinductive definition that can be used to define
-- various forms of similarity.

import Similarity.General

-- For more information about similarity, see "Similarity, continued"
-- below.

------------------------------------------------------------------------
-- Strong bisimilarity

-- The Step function, used to define strong and weak bisimilarity as
-- well as expansion.

import Bisimilarity.Step

-- A parametrised coinductive definition that can be used to define
-- strong and weak bisimilarity as well as expansion.

import Bisimilarity.General

-- A coinductive definition of (strong) bisimilarity.

import Bisimilarity
import Bisimilarity.Equational-reasoning-instances

-- The classical definition of (strong) bisimilarity.

import Bisimilarity.Classical
import Bisimilarity.Classical.Equational-reasoning-instances

-- A comparison of the two definitions of bisimilarity.

import Bisimilarity.Comparison

-- Some results related to strong bisimilarity for the delay monad.

import Bisimilarity.Delay-monad

-- Some results related to CCS, implemented without using a fixed form
-- of bisimilarity.

import Bisimilarity.CCS.General

-- Various results or examples related to CCS, implemented using the
-- coinductive definition of bisimilarity.

import Bisimilarity.CCS
import Bisimilarity.CCS.Examples
import Bisimilarity.CCS.Examples.Natural-numbers

-- Some of the results/examples above have also been implemented using
-- the classical definition of bisimilarity.

import Bisimilarity.CCS.Classical
import Bisimilarity.CCS.Examples.Classical

-- Up-to techniques for strong bisimilarity.

import Bisimilarity.Up-to
import Bisimilarity.Up-to.CCS
import Bisimilarity.Up-to.Counterexamples

-- Some results related to an LTS from Section 6.2.5 of "Enhancements
-- of the bisimulation proof method" by Pous and Sangiorgi,
-- implemented using the coinductive definition of bisimilarity.

import Bisimilarity.6-2-5

------------------------------------------------------------------------
-- Expansion

-- A coinductive definition of the expansion ordering.

import Expansion
import Expansion.Equational-reasoning-instances

-- Lemmas related to expansion and CCS.

import Expansion.CCS

-- Some results related to expansion for the delay monad.

import Expansion.Delay-monad

------------------------------------------------------------------------
-- Weak bisimilarity

-- A coinductive definition of weak bisimilarity.

import Bisimilarity.Weak
import Bisimilarity.Weak.Equational-reasoning-instances

-- An alternative (non-standard) coinductive definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative
import Bisimilarity.Weak.Alternative.Equational-reasoning-instances

-- An alternative (non-standard) classical definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative.Classical

-- A comparison of the two alternative definitions of weak
-- bisimilarity.

import Bisimilarity.Weak.Alternative.Comparison

-- The two coinductive definitions of weak bisimilarity are pointwise
-- logically equivalent.

import Bisimilarity.Weak.Equivalent

-- Lemmas related to weak bisimilarity and CCS.

import Bisimilarity.Weak.CCS

-- Examples/exercises related to CCS from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

import Bisimilarity.Weak.CCS.Examples

-- Some results about various forms of coinductively defined weak
-- bisimilarity for the delay monad.

import Bisimilarity.Weak.Delay-monad

-- Up-to techniques for the standard coinductive definition of weak
-- bisimilarity.

import Bisimilarity.Weak.Up-to
import Bisimilarity.Weak.Up-to.CCS

-- Up-to techniques for the delay monad and the alternative
-- coinductive definition of weak bisimilarity.

import Bisimilarity.Weak.Alternative.Up-to.Delay-monad

------------------------------------------------------------------------
-- Similarity, continued

-- A coinductive definition of (strong) similarity.

import Similarity
import Similarity.Equational-reasoning-instances

-- Lemmas related to strong similarity for CCS.

import Similarity.CCS

-- A coinductive definition of weak similarity.

import Similarity.Weak
import Similarity.Weak.Equational-reasoning-instances

-- An up-to technique for weak similarity.

import Similarity.Weak.Up-to