Index of /~nad/listings/chi

	Name	Last modified	Size	Description
	Parent Directory		-
	Accessibility.html	2025-09-19 17:41	94K
	Agda.Builtin.Bool.html	2025-09-19 17:41	3.1K
	Agda.Builtin.Char.html	2025-09-19 17:41	4.0K
	Agda.Builtin.Cubical..>	2025-09-19 17:42	53K
	Agda.Builtin.Cubical..>	2025-09-19 17:42	9.7K
	Agda.Builtin.Cubical..>	2025-09-19 17:42	53K
	Agda.Builtin.Cubical..>	2025-09-19 17:42	3.2K
	Agda.Builtin.Cubical..>	2025-09-19 17:42	5.1K
	Agda.Builtin.Equalit..>	2025-09-19 17:41	2.6K
	Agda.Builtin.Float.html	2025-09-19 17:42	32K
	Agda.Builtin.Int.html	2025-09-19 17:41	3.4K
	Agda.Builtin.List.html	2025-09-19 17:41	4.7K
	Agda.Builtin.Maybe.html	2025-09-19 17:41	2.3K
	Agda.Builtin.Nat.html	2025-09-19 17:41	23K
	Agda.Builtin.Reflect..>	2025-09-19 17:42	164K
	Agda.Builtin.Sigma.html	2025-09-19 17:41	3.4K
	Agda.Builtin.Strict...>	2025-09-19 17:42	4.8K
	Agda.Builtin.String...>	2025-09-19 17:41	10K
	Agda.Builtin.Unit.html	2025-09-19 17:41	1.7K
	Agda.Builtin.Word.html	2025-09-19 17:42	2.0K
	Agda.Primitive.Cubic..>	2025-09-19 17:42	24K
	Agda.Primitive.html	2025-09-19 17:41	5.4K
	Agda.css	2025-09-19 17:41	1.8K
	Algebra.Bundles.Raw...>	2025-09-19 17:41	66K
	Algebra.Bundles.html	2025-09-19 17:41	282K
	Algebra.Consequences..>	2025-09-19 17:41	15K
	Algebra.Consequences..>	2025-09-19 17:41	48K
	Algebra.Consequences..>	2025-09-19 17:41	179K
	Algebra.Construct.Li..>	2025-09-19 17:42	84K
	Algebra.Construct.Na..>	2025-09-19 17:41	17K
	Algebra.Construct.Na..>	2025-09-19 17:42	7.5K
	Algebra.Construct.Na..>	2025-09-19 17:41	18K
	Algebra.Construct.Na..>	2025-09-19 17:42	13K
	Algebra.Construct.Na..>	2025-09-19 17:42	56K
	Algebra.Construct.Na..>	2025-09-19 17:41	109K
	Algebra.Core.html	2025-09-19 17:41	3.3K
	Algebra.Definitions...>	2025-09-19 17:41	19K
	Algebra.Definitions...>	2025-09-19 17:42	11K
	Algebra.Definitions...>	2025-09-19 17:42	21K
	Algebra.Definitions...>	2025-09-19 17:41	117K
	Algebra.Lattice.Bund..>	2025-09-19 17:41	7.4K
	Algebra.Lattice.Bund..>	2025-09-19 17:41	53K
	Algebra.Lattice.Cons..>	2025-09-19 17:42	4.8K
	Algebra.Lattice.Cons..>	2025-09-19 17:42	19K
	Algebra.Lattice.Cons..>	2025-09-19 17:41	6.5K
	Algebra.Lattice.Prop..>	2025-09-19 17:42	293K
	Algebra.Lattice.Prop..>	2025-09-19 17:42	6.2K
	Algebra.Lattice.Prop..>	2025-09-19 17:42	43K
	Algebra.Lattice.Prop..>	2025-09-19 17:42	11K
	Algebra.Lattice.Stru..>	2025-09-19 17:41	40K
	Algebra.Morphism.Def..>	2025-09-19 17:41	11K
	Algebra.Morphism.Str..>	2025-09-19 17:42	210K
	Algebra.Morphism.html	2025-09-19 17:42	47K
	Algebra.Properties.A..>	2025-09-19 17:41	13K
	Algebra.Properties.C..>	2025-09-19 17:42	112K
	Algebra.Properties.G..>	2025-09-19 17:41	70K
	Algebra.Properties.L..>	2025-09-19 17:41	15K
	Algebra.Properties.M..>	2025-09-19 17:42	32K
	Algebra.Properties.Q..>	2025-09-19 17:41	16K
	Algebra.Properties.R..>	2025-09-19 17:41	6.4K
	Algebra.Properties.R..>	2025-09-19 17:41	44K
	Algebra.Properties.S..>	2025-09-19 17:42	56K
	Algebra.Properties.S..>	2025-09-19 17:42	39K
	Algebra.Solver.Ring...>	2025-09-19 17:41	45K
	Algebra.Solver.Ring...>	2025-09-19 17:42	96K
	Algebra.Solver.Ring...>	2025-09-19 17:42	4.6K
	Algebra.Solver.Ring...>	2025-09-19 17:42	288K
	Algebra.Structures.B..>	2025-09-19 17:41	65K
	Algebra.Structures.html	2025-09-19 17:41	233K
	Algebra.html	2025-09-19 17:41	1.9K
	Alpha-equivalence.html	2025-09-19 17:42	761K
	Atom.html	2025-09-19 17:42	47K
	Axiom.Extensionality..>	2025-09-19 17:41	21K
	Axiom.UniquenessOfId..>	2025-09-19 17:41	21K
	Bag-equivalence.html	2025-09-19 17:42	648K
	Bijection.html	2025-09-19 17:41	226K
	Bool.html	2025-09-19 17:41	74K
	Cancellation.html	2025-09-19 17:42	15K
	Chi.html	2025-09-19 17:42	40K
	Coding.Instances.Nat..>	2025-09-19 17:42	1.4K
	Coding.Instances.html	2025-09-19 17:42	14K
	Coding.html	2025-09-19 17:42	296K
	Colimit.Sequential.V..>	2025-09-19 17:42	179K
	Combinators.html	2025-09-19 17:42	206K
	Compatibility.html	2025-09-19 17:42	55K
	Computability.html	2025-09-19 17:42	276K
	Computable-function...>	2025-09-19 17:42	49K
	Constants.html	2025-09-19 17:42	17K
	Data.Bool.Base.html	2025-09-19 17:41	13K
	Data.Bool.ListAction..>	2025-09-19 17:42	7.3K
	Data.Bool.Properties..>	2025-09-19 17:42	245K
	Data.Empty.Polymorph..>	2025-09-19 17:41	4.5K
	Data.Empty.html	2025-09-19 17:41	5.0K
	Data.Fin.Base.html	2025-09-19 17:41	119K
	Data.Fin.Patterns.html	2025-09-19 17:42	4.7K
	Data.Fin.Properties...>	2025-09-19 17:42	597K
	Data.Irrelevant.html	2025-09-19 17:41	12K
	Data.List.Base.html	2025-09-19 17:41	223K
	Data.List.Effectful...>	2025-09-19 17:42	147K
	Data.List.Extrema.Co..>	2025-09-19 17:42	62K
	Data.List.Extrema.html	2025-09-19 17:42	132K
	Data.List.Membership..>	2025-09-19 17:42	44K
	Data.List.Membership..>	2025-09-19 17:42	239K
	Data.List.Membership..>	2025-09-19 17:42	9.3K
	Data.List.Membership..>	2025-09-19 17:42	261K
	Data.List.Membership..>	2025-09-19 17:42	20K
	Data.List.Properties..>	2025-09-19 17:42	889K
	Data.List.Relation.B..>	2025-09-19 17:42	6.9K
	Data.List.Relation.B..>	2025-09-19 17:42	51K
	Data.List.Relation.B..>	2025-09-19 17:42	31K
	Data.List.Relation.B..>	2025-09-19 17:42	46K
	Data.List.Relation.B..>	2025-09-19 17:42	130K
	Data.List.Relation.B..>	2025-09-19 17:42	2.8K
	Data.List.Relation.B..>	2025-09-19 17:42	11K
	Data.List.Relation.U..>	2025-09-19 17:42	49K
	Data.List.Relation.U..>	2025-09-19 17:42	388K
	Data.List.Relation.U..>	2025-09-19 17:42	112K
	Data.List.Relation.U..>	2025-09-19 17:42	6.3K
	Data.List.Relation.U..>	2025-09-19 17:42	36K
	Data.List.Relation.U..>	2025-09-19 17:42	459K
	Data.List.Relation.U..>	2025-09-19 17:42	38K
	Data.List.Relation.U..>	2025-09-19 17:42	3.8K
	Data.Maybe.Base.html	2025-09-19 17:41	37K
	Data.Maybe.Relation...>	2025-09-19 17:42	56K
	Data.Maybe.Relation...>	2025-09-19 17:42	32K
	Data.Nat.Base.html	2025-09-19 17:41	103K
	Data.Nat.DivMod.Core..>	2025-09-19 17:42	224K
	Data.Nat.DivMod.html	2025-09-19 17:42	356K
	Data.Nat.Divisibilit..>	2025-09-19 17:42	16K
	Data.Nat.Divisibilit..>	2025-09-19 17:42	170K
	Data.Nat.Generalised..>	2025-09-19 17:42	68K
	Data.Nat.Induction.html	2025-09-19 17:42	25K
	Data.Nat.Properties...>	2025-09-19 17:42	935K
	Data.Nat.Solver.html	2025-09-19 17:42	2.4K
	Data.Parity.Base.html	2025-09-19 17:41	19K
	Data.Product.Algebra..>	2025-09-19 17:42	55K
	Data.Product.Base.html	2025-09-19 17:41	87K
	Data.Product.Functio..>	2025-09-19 17:42	168K
	Data.Product.Functio..>	2025-09-19 17:42	49K
	Data.Product.Functio..>	2025-09-19 17:42	59K
	Data.Product.Propert..>	2025-09-19 17:42	57K
	Data.Product.Relatio..>	2025-09-19 17:42	97K
	Data.Product.Relatio..>	2025-09-19 17:42	5.4K
	Data.Sign.Base.html	2025-09-19 17:41	8.9K
	Data.Sum.Algebra.html	2025-09-19 17:42	33K
	Data.Sum.Base.html	2025-09-19 17:41	26K
	Data.Sum.Function.Pr..>	2025-09-19 17:42	46K
	Data.Sum.Function.Se..>	2025-09-19 17:42	73K
	Data.Sum.Properties...>	2025-09-19 17:42	60K
	Data.Sum.Relation.Bi..>	2025-09-19 17:42	116K
	Data.Sum.html	2025-09-19 17:42	12K
	Data.These.Base.html	2025-09-19 17:41	37K
	Data.Unit.Base.html	2025-09-19 17:41	1.9K
	Data.Unit.Polymorphi..>	2025-09-19 17:41	3.6K
	Data.Unit.Polymorphi..>	2025-09-19 17:42	27K
	Data.Unit.Polymorphi..>	2025-09-19 17:42	1.9K
	Data.Vec.Base.html	2025-09-19 17:41	150K
	Data.Vec.Bounded.Bas..>	2025-09-19 17:42	68K
	Data.Vec.Functional...>	2025-09-19 17:42	67K
	Data.Vec.N-ary.html	2025-09-19 17:41	92K
	Data.Vec.html	2025-09-19 17:42	12K
	Dec.html	2025-09-19 17:42	12K
	Decidable.html	2025-09-19 17:42	174K
	Derivation-size.html	2025-09-19 17:42	107K
	Deterministic.html	2025-09-19 17:42	50K
	Double-negation.html	2025-09-19 17:42	96K
	Effect.Applicative.html	2025-09-19 17:41	36K
	Effect.Choice.html	2025-09-19 17:41	4.4K
	Effect.Empty.html	2025-09-19 17:41	3.8K
	Effect.Functor.html	2025-09-19 17:41	13K
	Effect.Monad.html	2025-09-19 17:41	35K
	Embedding.Erased.html	2025-09-19 17:42	67K
	Embedding.html	2025-09-19 17:41	93K
	Equality.Decidable-U..>	2025-09-19 17:41	76K
	Equality.Decision-pr..>	2025-09-19 17:41	97K
	Equality.Groupoid.html	2025-09-19 17:42	100K
	Equality.Instances-r..>	2025-09-19 17:42	120K
	Equality.Path.Isomor..>	2025-09-19 17:42	5.5K
	Equality.Path.Isomor..>	2025-09-19 17:42	259K
	Equality.Path.Unival..>	2025-09-19 17:42	66K
	Equality.Path.html	2025-09-19 17:42	347K
	Equality.Proposition..>	2025-09-19 17:42	10K
	Equality.Proposition..>	2025-09-19 17:41	19K
	Equality.Tactic.html	2025-09-19 17:42	129K
	Equality.html	2025-09-19 17:41	1.0M
	Equivalence-relation..>	2025-09-19 17:41	82K
	Equivalence.Contract..>	2025-09-19 17:41	128K
	Equivalence.Erased.B..>	2025-09-19 17:41	97K
	Equivalence.Erased.C..>	2025-09-19 17:41	71K
	Equivalence.Erased.C..>	2025-09-19 17:42	155K
	Equivalence.Erased.C..>	2025-09-19 17:42	3.4K
	Equivalence.Erased.html	2025-09-19 17:42	880K
	Equivalence.Half-adj..>	2025-09-19 17:41	133K
	Equivalence.List.html	2025-09-19 17:42	355K
	Equivalence.Path-spl..>	2025-09-19 17:42	413K
	Equivalence.html	2025-09-19 17:41	502K
	Erased.Basics.html	2025-09-19 17:41	14K
	Erased.Box-cong-axio..>	2025-09-19 17:41	7.0K
	Erased.Cubical.html	2025-09-19 17:42	49K
	Erased.Level-1.html	2025-09-19 17:42	1.2M
	Erased.Level-2.html	2025-09-19 17:42	334K
	Erased.Stability.html	2025-09-19 17:42	1.2M
	Erased.html	2025-09-19 17:42	6.2K
	Excluded-middle.html	2025-09-19 17:41	6.6K
	Expression-size.html	2025-09-19 17:42	58K
	Extensionality.html	2025-09-19 17:41	189K
	Fin.html	2025-09-19 17:42	183K
	Finite-subset.Listed..>	2025-09-19 17:42	425K
	Finite-subset.Listed..>	2025-09-19 17:42	650K
	Finite-subset.Listed..>	2025-09-19 17:42	270K
	For-iterated-equalit..>	2025-09-19 17:42	337K
	Free-variables.Remov..>	2025-09-19 17:42	121K
	Free-variables.html	2025-09-19 17:42	666K
	Function-universe.html	2025-09-19 17:41	2.6M
	Function.Base.html	2025-09-19 17:41	76K
	Function.Bundles.html	2025-09-19 17:41	128K
	Function.Consequence..>	2025-09-19 17:41	12K
	Function.Consequence..>	2025-09-19 17:41	23K
	Function.Consequence..>	2025-09-19 17:41	35K
	Function.Construct.C..>	2025-09-19 17:42	119K
	Function.Construct.I..>	2025-09-19 17:42	46K
	Function.Construct.S..>	2025-09-19 17:42	72K
	Function.Core.html	2025-09-19 17:42	5.0K
	Function.Definitions..>	2025-09-19 17:41	21K
	Function.Dependent.B..>	2025-09-19 17:41	9.3K
	Function.Indexed.Rel..>	2025-09-19 17:41	8.2K
	Function.Metric.Bund..>	2025-09-19 17:42	37K
	Function.Metric.Core..>	2025-09-19 17:42	2.8K
	Function.Metric.Defi..>	2025-09-19 17:42	35K
	Function.Metric.Nat...>	2025-09-19 17:42	29K
	Function.Metric.Nat...>	2025-09-19 17:42	2.8K
	Function.Metric.Nat...>	2025-09-19 17:42	18K
	Function.Metric.Nat...>	2025-09-19 17:42	19K
	Function.Metric.Nat...>	2025-09-19 17:42	1.8K
	Function.Metric.Stru..>	2025-09-19 17:42	22K
	Function.Properties...>	2025-09-19 17:42	21K
	Function.Properties...>	2025-09-19 17:42	46K
	Function.Properties...>	2025-09-19 17:42	54K
	Function.Properties...>	2025-09-19 17:42	20K
	Function.Properties...>	2025-09-19 17:42	24K
	Function.Related.Pro..>	2025-09-19 17:42	123K
	Function.Related.Typ..>	2025-09-19 17:42	162K
	Function.Structures...>	2025-09-19 17:41	47K
	Groupoid.html	2025-09-19 17:41	193K
	H-level.Closure.html	2025-09-19 17:41	406K
	H-level.Truncation.C..>	2025-09-19 17:42	584K
	H-level.Truncation.P..>	2025-09-19 17:42	417K
	H-level.Truncation.P..>	2025-09-19 17:42	277K
	H-level.Truncation.P..>	2025-09-19 17:42	157K
	H-level.Truncation.P..>	2025-09-19 17:42	246K
	H-level.Truncation.P..>	2025-09-19 17:42	558K
	H-level.html	2025-09-19 17:41	53K
	Halting-problem.html	2025-09-19 17:42	258K
	Induction.WellFounde..>	2025-09-19 17:42	96K
	Induction.html	2025-09-19 17:42	14K
	Injection.html	2025-09-19 17:41	18K
	Integer.Basics.html	2025-09-19 17:41	40K
	Internal-coding.html	2025-09-19 17:42	194K
	Internal-lookup.html	2025-09-19 17:42	166K
	Internal-substitutio..>	2025-09-19 17:42	437K
	Level.html	2025-09-19 17:41	5.6K
	List.All.html	2025-09-19 17:42	221K
	List.html	2025-09-19 17:42	265K
	Logical-equivalence...>	2025-09-19 17:41	50K
	Maybe.html	2025-09-19 17:41	52K
	Modality.Basics.html	2025-09-19 17:42	2.1M
	Modality.Box-cong.html	2025-09-19 17:42	59K
	Modality.Commutes-wi..>	2025-09-19 17:42	189K
	Modality.Empty-modal..>	2025-09-19 17:42	150K
	Modality.Has-choice...>	2025-09-19 17:42	862K
	Modality.Identity.html	2025-09-19 17:42	17K
	Modality.Left-exact...>	2025-09-19 17:42	238K
	Modality.Very-modal...>	2025-09-19 17:42	268K
	Monad.Raw.html	2025-09-19 17:41	18K
	Monad.State.html	2025-09-19 17:42	37K
	Monad.html	2025-09-19 17:41	115K
	Nat.Solver.html	2025-09-19 17:42	59K
	Nat.html	2025-09-19 17:41	476K
	Not-the-code-of.html	2025-09-19 17:42	127K
	Pointed-type.html	2025-09-19 17:42	198K
	Pointwise-equality.html	2025-09-19 17:42	189K
	Preimage.html	2025-09-19 17:41	59K
	Prelude.html	2025-09-19 17:41	123K
	Propositional.html	2025-09-19 17:42	162K
	Pullback.html	2025-09-19 17:42	102K
	Quotient.Erased.Basi..>	2025-09-19 17:42	87K
	Quotient.Erased.html	2025-09-19 17:42	268K
	Quotient.Families-of..>	2025-09-19 17:42	484K
	Quotient.html	2025-09-19 17:42	430K
	Reasoning.html	2025-09-19 17:42	20K
	Recursion-without-re..>	2025-09-19 17:42	166K
	Relation.Binary.Bund..>	2025-09-19 17:41	12K
	Relation.Binary.Bund..>	2025-09-19 17:41	98K
	Relation.Binary.Cons..>	2025-09-19 17:41	109K
	Relation.Binary.Cons..>	2025-09-19 17:41	50K
	Relation.Binary.Cons..>	2025-09-19 17:41	77K
	Relation.Binary.Cons..>	2025-09-19 17:42	82K
	Relation.Binary.Cons..>	2025-09-19 17:42	80K
	Relation.Binary.Cons..>	2025-09-19 17:41	73K
	Relation.Binary.Core..>	2025-09-19 17:41	19K
	Relation.Binary.Defi..>	2025-09-19 17:41	101K
	Relation.Binary.Inde..>	2025-09-19 17:41	12K
	Relation.Binary.Inde..>	2025-09-19 17:41	17K
	Relation.Binary.Inde..>	2025-09-19 17:41	13K
	Relation.Binary.Inde..>	2025-09-19 17:41	11K
	Relation.Binary.Inde..>	2025-09-19 17:41	14K
	Relation.Binary.Inde..>	2025-09-19 17:41	2.1K
	Relation.Binary.Latt..>	2025-09-19 17:42	69K
	Relation.Binary.Latt..>	2025-09-19 17:42	13K
	Relation.Binary.Latt..>	2025-09-19 17:42	63K
	Relation.Binary.Latt..>	2025-09-19 17:42	1.7K
	Relation.Binary.Morp..>	2025-09-19 17:42	6.3K
	Relation.Binary.Morp..>	2025-09-19 17:42	38K
	Relation.Binary.Prop..>	2025-09-19 17:42	16K
	Relation.Binary.Prop..>	2025-09-19 17:41	34K
	Relation.Binary.Prop..>	2025-09-19 17:41	11K
	Relation.Binary.Prop..>	2025-09-19 17:41	24K
	Relation.Binary.Prop..>	2025-09-19 17:41	18K
	Relation.Binary.Prop..>	2025-09-19 17:41	7.0K
	Relation.Binary.Prop..>	2025-09-19 17:41	37K
	Relation.Binary.Prop..>	2025-09-19 17:41	110K
	Relation.Binary.Prop..>	2025-09-19 17:41	51K
	Relation.Binary.Reas..>	2025-09-19 17:41	32K
	Relation.Binary.Reas..>	2025-09-19 17:41	14K
	Relation.Binary.Reas..>	2025-09-19 17:42	54K
	Relation.Binary.Reas..>	2025-09-19 17:41	3.7K
	Relation.Binary.Reas..>	2025-09-19 17:41	5.4K
	Relation.Binary.Reas..>	2025-09-19 17:41	90K
	Relation.Binary.Refl..>	2025-09-19 17:41	37K
	Relation.Binary.Stru..>	2025-09-19 17:41	10K
	Relation.Binary.Stru..>	2025-09-19 17:41	68K
	Relation.Binary.html	2025-09-19 17:42	2.1K
	Relation.Nullary.Dec..>	2025-09-19 17:41	71K
	Relation.Nullary.Dec..>	2025-09-19 17:41	42K
	Relation.Nullary.Ind..>	2025-09-19 17:42	3.2K
	Relation.Nullary.Irr..>	2025-09-19 17:41	3.2K
	Relation.Nullary.Neg..>	2025-09-19 17:41	22K
	Relation.Nullary.Neg..>	2025-09-19 17:41	38K
	Relation.Nullary.Rec..>	2025-09-19 17:41	8.3K
	Relation.Nullary.Rec..>	2025-09-19 17:41	16K
	Relation.Nullary.Ref..>	2025-09-19 17:41	45K
	Relation.Nullary.html	2025-09-19 17:41	5.1K
	Relation.Unary.Predi..>	2025-09-19 17:42	44K
	Relation.Unary.Prope..>	2025-09-19 17:42	132K
	Relation.Unary.html	2025-09-19 17:41	96K
	Rices-theorem.html	2025-09-19 17:42	163K
	Self-interpreter.html	2025-09-19 17:42	472K
	Substitution.html	2025-09-19 17:42	65K
	Sum.html	2025-09-19 17:42	13K
	Surjection.html	2025-09-19 17:41	88K
	TC-monad.html	2025-09-19 17:42	171K
	Tactic.By.Propositio..>	2025-09-19 17:42	121K
	Tactic.By.html	2025-09-19 17:42	145K
	Tactic.Sigma-cong.html	2025-09-19 17:42	159K
	Termination.html	2025-09-19 17:42	16K
	Univalence-axiom.html	2025-09-19 17:41	707K
	Values.html	2025-09-19 17:42	24K
	Vec.Dependent.html	2025-09-19 17:42	47K
	Vec.Function.html	2025-09-19 17:42	47K

------------------------------------------------------------------------
-- 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