Index of /~nad/listings/chi

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

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