Index of /~nad/listings/chi

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory   -  
[TXT]Accessibility.html 2023-09-29 17:41 94K 
[TXT]Agda.Builtin.Bool.html 2023-09-29 17:41 3.1K 
[TXT]Agda.Builtin.Char.html 2023-09-29 17:41 4.0K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:41 53K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:41 9.7K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:41 53K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:41 3.2K 
[TXT]Agda.Builtin.Cubical..>2023-09-29 17:41 5.1K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:41 2.6K 
[TXT]Agda.Builtin.Float.html2023-09-29 17:41 32K 
[TXT]Agda.Builtin.Int.html 2023-09-29 17:41 3.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.Reflect..>2023-09-29 17:41 160K 
[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 10K 
[TXT]Agda.Builtin.Unit.html 2023-09-29 17:41 1.7K 
[TXT]Agda.Builtin.Word.html 2023-09-29 17:41 2.0K 
[TXT]Agda.Primitive.Cubic..>2023-09-29 17:41 24K 
[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 41K 
[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]Alpha-equivalence.html 2023-09-29 17:41 750K 
[TXT]Atom.html 2023-09-29 17:41 47K 
[TXT]Axiom.Extensionality..>2023-09-29 17:41 21K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:41 23K 
[TXT]Bag-equivalence.html 2023-09-29 17:41 647K 
[TXT]Bijection.html 2023-09-29 17:41 226K 
[TXT]Bool.html 2023-09-29 17:41 74K 
[TXT]Cancellation.html 2023-09-29 17:41 15K 
[TXT]Chi.html 2023-09-29 17:41 40K 
[TXT]Coding.Instances.Nat..>2023-09-29 17:41 1.4K 
[TXT]Coding.Instances.html 2023-09-29 17:41 13K 
[TXT]Coding.html 2023-09-29 17:41 298K 
[TXT]Colimit.Sequential.V..>2023-09-29 17:41 179K 
[TXT]Combinators.html 2023-09-29 17:41 206K 
[TXT]Compatibility.html 2023-09-29 17:41 55K 
[TXT]Computability.html 2023-09-29 17:41 276K 
[TXT]Computable-function...>2023-09-29 17:41 49K 
[TXT]Constants.html 2023-09-29 17:41 17K 
[TXT]Data.Bool.Base.html 2023-09-29 17:41 13K 
[TXT]Data.Bool.Properties..>2023-09-29 17:41 204K 
[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.Irrelevant.html 2023-09-29 17:41 12K 
[TXT]Data.List.Base.html 2023-09-29 17:41 194K 
[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 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.Properties..>2023-09-29 17:41 618K 
[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 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 2.8K 
[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.Maybe.Base.html 2023-09-29 17:41 37K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:41 54K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:41 31K 
[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.Properties...>2023-09-29 17:41 908K 
[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.Sign.Base.html 2023-09-29 17:41 8.9K 
[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.These.Base.html 2023-09-29 17:41 36K 
[TXT]Data.Unit.Base.html 2023-09-29 17:41 1.9K 
[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.Functional...>2023-09-29 17:41 69K 
[TXT]Data.Vec.N-ary.html 2023-09-29 17:41 92K 
[TXT]Data.Vec.html 2023-09-29 17:41 12K 
[TXT]Dec.html 2023-09-29 17:41 12K 
[TXT]Decidable.html 2023-09-29 17:41 174K 
[TXT]Derivation-size.html 2023-09-29 17:41 107K 
[TXT]Deterministic.html 2023-09-29 17:41 50K 
[TXT]Double-negation.html 2023-09-29 17:41 96K 
[TXT]Effect.Applicative.html2023-09-29 17:41 36K 
[TXT]Effect.Choice.html 2023-09-29 17:41 4.4K 
[TXT]Effect.Empty.html 2023-09-29 17:41 3.4K 
[TXT]Effect.Functor.html 2023-09-29 17:41 13K 
[TXT]Effect.Monad.html 2023-09-29 17:41 32K 
[TXT]Embedding.Erased.html 2023-09-29 17:41 67K 
[TXT]Embedding.html 2023-09-29 17:41 82K 
[TXT]Equality.Decidable-U..>2023-09-29 17:41 76K 
[TXT]Equality.Decision-pr..>2023-09-29 17:41 97K 
[TXT]Equality.Groupoid.html 2023-09-29 17:41 100K 
[TXT]Equality.Instances-r..>2023-09-29 17:41 120K 
[TXT]Equality.Path.Isomor..>2023-09-29 17:41 6.2K 
[TXT]Equality.Path.Isomor..>2023-09-29 17:41 259K 
[TXT]Equality.Path.Unival..>2023-09-29 17:41 66K 
[TXT]Equality.Path.html 2023-09-29 17:41 342K 
[TXT]Equality.Proposition..>2023-09-29 17:41 10K 
[TXT]Equality.Proposition..>2023-09-29 17:41 19K 
[TXT]Equality.Tactic.html 2023-09-29 17:41 129K 
[TXT]Equality.html 2023-09-29 17:41 1.0M 
[TXT]Equivalence-relation..>2023-09-29 17:41 82K 
[TXT]Equivalence.Contract..>2023-09-29 17:41 128K 
[TXT]Equivalence.Erased.B..>2023-09-29 17:41 97K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:41 70K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:41 151K 
[TXT]Equivalence.Erased.C..>2023-09-29 17:41 3.4K 
[TXT]Equivalence.Erased.html2023-09-29 17:41 689K 
[TXT]Equivalence.Half-adj..>2023-09-29 17:41 133K 
[TXT]Equivalence.List.html 2023-09-29 17:41 355K 
[TXT]Equivalence.Path-spl..>2023-09-29 17:41 413K 
[TXT]Equivalence.html 2023-09-29 17:41 502K 
[TXT]Erased.Basics.html 2023-09-29 17:41 14K 
[TXT]Erased.Box-cong-axio..>2023-09-29 17:41 7.0K 
[TXT]Erased.Cubical.html 2023-09-29 17:41 53K 
[TXT]Erased.Level-1.html 2023-09-29 17:41 1.0M 
[TXT]Erased.Level-2.html 2023-09-29 17:41 298K 
[TXT]Erased.Stability.html 2023-09-29 17:41 1.0M 
[TXT]Erased.html 2023-09-29 17:41 6.1K 
[TXT]Excluded-middle.html 2023-09-29 17:41 6.6K 
[TXT]Expression-size.html 2023-09-29 17:41 58K 
[TXT]Extensionality.html 2023-09-29 17:41 189K 
[TXT]Fin.html 2023-09-29 17:41 182K 
[TXT]Finite-subset.Listed..>2023-09-29 17:41 425K 
[TXT]Finite-subset.Listed..>2023-09-29 17:41 650K 
[TXT]Finite-subset.Listed..>2023-09-29 17:41 270K 
[TXT]For-iterated-equalit..>2023-09-29 17:41 337K 
[TXT]Free-variables.Remov..>2023-09-29 17:41 121K 
[TXT]Free-variables.html 2023-09-29 17:41 665K 
[TXT]Function-universe.html 2023-09-29 17:41 2.5M 
[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.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 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.Structures...>2023-09-29 17:41 43K 
[TXT]Function.Surjection...>2023-09-29 17:41 33K 
[TXT]Groupoid.html 2023-09-29 17:41 189K 
[TXT]H-level.Closure.html 2023-09-29 17:41 406K 
[TXT]H-level.Truncation.C..>2023-09-29 17:41 583K 
[TXT]H-level.Truncation.P..>2023-09-29 17:41 418K 
[TXT]H-level.Truncation.P..>2023-09-29 17:41 275K 
[TXT]H-level.Truncation.P..>2023-09-29 17:41 157K 
[TXT]H-level.Truncation.P..>2023-09-29 17:41 246K 
[TXT]H-level.Truncation.P..>2023-09-29 17:41 557K 
[TXT]H-level.html 2023-09-29 17:41 53K 
[TXT]Halting-problem.html 2023-09-29 17:41 258K 
[TXT]Induction.WellFounde..>2023-09-29 17:41 87K 
[TXT]Induction.html 2023-09-29 17:41 17K 
[TXT]Injection.html 2023-09-29 17:41 18K 
[TXT]Integer.Basics.html 2023-09-29 17:41 40K 
[TXT]Internal-coding.html 2023-09-29 17:41 194K 
[TXT]Internal-lookup.html 2023-09-29 17:41 166K 
[TXT]Internal-substitutio..>2023-09-29 17:41 437K 
[TXT]Level.html 2023-09-29 17:41 5.6K 
[TXT]List.All.html 2023-09-29 17:41 221K 
[TXT]List.html 2023-09-29 17:41 265K 
[TXT]Logical-equivalence...>2023-09-29 17:41 50K 
[TXT]Maybe.html 2023-09-29 17:41 52K 
[TXT]Modality.Basics.html 2023-09-29 17:41 2.1M 
[TXT]Modality.Box-cong.html 2023-09-29 17:41 58K 
[TXT]Modality.Commutes-wi..>2023-09-29 17:41 189K 
[TXT]Modality.Empty-modal..>2023-09-29 17:41 150K 
[TXT]Modality.Has-choice...>2023-09-29 17:41 861K 
[TXT]Modality.Identity.html 2023-09-29 17:41 17K 
[TXT]Modality.Left-exact...>2023-09-29 17:41 238K 
[TXT]Modality.Very-modal...>2023-09-29 17:41 250K 
[TXT]Monad.Raw.html 2023-09-29 17:41 18K 
[TXT]Monad.State.html 2023-09-29 17:41 37K 
[TXT]Monad.html 2023-09-29 17:41 115K 
[TXT]Nat.Solver.html 2023-09-29 17:41 59K 
[TXT]Nat.html 2023-09-29 17:41 476K 
[TXT]Not-the-code-of.html 2023-09-29 17:41 127K 
[TXT]Pointed-type.html 2023-09-29 17:41 197K 
[TXT]Pointwise-equality.html2023-09-29 17:41 189K 
[TXT]Preimage.html 2023-09-29 17:41 59K 
[TXT]Prelude.html 2023-09-29 17:41 123K 
[TXT]Propositional.html 2023-09-29 17:41 162K 
[TXT]Pullback.html 2023-09-29 17:41 102K 
[TXT]Quotient.Erased.Basi..>2023-09-29 17:41 88K 
[TXT]Quotient.Erased.html 2023-09-29 17:41 269K 
[TXT]Quotient.Families-of..>2023-09-29 17:41 484K 
[TXT]Quotient.html 2023-09-29 17:41 425K 
[TXT]Reasoning.html 2023-09-29 17:41 20K 
[TXT]Recursion-without-re..>2023-09-29 17:41 166K 
[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 72K 
[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.Core..>2023-09-29 17:41 19K 
[TXT]Relation.Binary.Defi..>2023-09-29 17:41 91K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:41 11K 
[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 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 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.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]Rices-theorem.html 2023-09-29 17:41 163K 
[TXT]Self-interpreter.html 2023-09-29 17:41 472K 
[TXT]Substitution.html 2023-09-29 17:41 65K 
[TXT]Sum.html 2023-09-29 17:41 13K 
[TXT]Surjection.html 2023-09-29 17:41 88K 
[TXT]TC-monad.html 2023-09-29 17:41 170K 
[TXT]Tactic.By.Propositio..>2023-09-29 17:41 121K 
[TXT]Tactic.By.html 2023-09-29 17:41 145K 
[TXT]Tactic.Sigma-cong.html 2023-09-29 17:41 158K 
[TXT]Termination.html 2023-09-29 17:41 16K 
[TXT]Univalence-axiom.html 2023-09-29 17:41 706K 
[TXT]Values.html 2023-09-29 17:41 24K 
[TXT]Vec.Dependent.html 2023-09-29 17:41 47K 
[TXT]Vec.Function.html 2023-09-29 17:41 47K 

README
------------------------------------------------------------------------
-- A formalisation of one variant of the language χ, along with a
-- number of properties
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- A description of the language χ, as well as some of the definitions
-- and proofs used in this development, can be found in "The language
-- χ" by Bengt Nordström (edited by me):
--
-- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/reading/The_language_chi.pdf
--
-- See also the following lecture slides:
--
-- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/lectures/L4.pdf
-- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/lectures/L5.pdf
-- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/lectures/L6.pdf

module README where

-- Atoms.

import Atom

-- Various constants.

import Constants

-- A specification of the language χ.

import Chi

-- Some cancellation lemmas.

import Cancellation

-- The semantics is deterministic.

import Deterministic

-- Values.

import Values

-- "Reasoning" combinators.

import Reasoning

-- The abstract syntax is a set, and the semantics is propositional.

import Propositional

-- Compatibility lemmas.

import Compatibility

-- Some lemmas and definitions related to substitution.

import Substitution

-- Definitions of "free in" and "closed", along with some properties.

import Free-variables

-- Alpha-equivalence.

import Alpha-equivalence

-- Encoders and decoders.

import Coding

-- Encoder and decoder instances.

import Coding.Instances

-- Encoder and decoder instances for Atom.χ-ℕ-atoms.

import Coding.Instances.Nat

-- The "not the code of" operator ⌞_⌟.

import Not-the-code-of

-- A tactic that can "remove" applications of substitutions to closed
-- expressions.

import Free-variables.Remove-substs

-- A definition of the size of an operational semantics derivation,
-- along with some properties.

import Derivation-size

-- The "terminates" relation.

import Termination

-- Some χ program combinators.

import Combinators

-- A definition of the size of an expression, along with some
-- properties.

import Expression-size

-- The rec construction can be encoded using λ-terms.

import Recursion-without-rec

-- Some aspects of the semantics are decidable.

import Decidable

-- Partial functions, computability.

import Computability

-- Computable Agda functions.

import Computable-function

-- Internal coding.

import Internal-coding

-- Internal substitution.

import Internal-substitution

-- Internal lookup.

import Internal-lookup

-- A self-interpreter.

import Self-interpreter

-- The halting problem.

import Halting-problem

-- Rice's theorem.

import Rices-theorem

-- Some results related to pointwise equality.

import Pointwise-equality