Project Page
Index
Table of Contents
Mcltt.Algorithmic.Subtyping.Definitions
Mcltt.Algorithmic.Subtyping.Lemmas
Mcltt.Algorithmic.Typing.Definitions
Mcltt.Algorithmic.Typing.Lemmas
Mcltt.Core.Base
Mcltt.Core.Completeness
Mcltt.Core.Completeness.Consequences.Inversions
Mcltt.Core.Completeness.Consequences.Rules
Mcltt.Core.Completeness.Consequences.Types
Mcltt.Core.Completeness.ContextCases
Mcltt.Core.Completeness.FunctionCases
Mcltt.Core.Completeness.FundamentalTheorem
Mcltt.Core.Completeness.LogicalRelation
Mcltt.Core.Completeness.LogicalRelation.Definitions
Mcltt.Core.Completeness.LogicalRelation.Lemmas
Mcltt.Core.Completeness.LogicalRelation.Tactics
Mcltt.Core.Completeness.NatCases
Mcltt.Core.Completeness.SubstitutionCases
Mcltt.Core.Completeness.SubtypingCases
Mcltt.Core.Completeness.TermStructureCases
Mcltt.Core.Completeness.UniverseCases
Mcltt.Core.Completeness.VariableCases
Mcltt.Core.Semantic.Consequences
Mcltt.Core.Semantic.Domain
Mcltt.Core.Semantic.Evaluation
Mcltt.Core.Semantic.Evaluation.Definitions
Mcltt.Core.Semantic.Evaluation.Lemmas
Mcltt.Core.Semantic.Evaluation.Tactics
Mcltt.Core.Semantic.NbE
Mcltt.Core.Semantic.PER
Mcltt.Core.Semantic.PER.CoreTactics
Mcltt.Core.Semantic.PER.Definitions
Universe/Element PER
Universe/Element PER Definition
Universe/Element PER Induction Principle
Universe Subtyping
Context/Environment PER
Context Subtyping
Mcltt.Core.Semantic.PER.Lemmas
Mcltt.Core.Semantic.Readback
Mcltt.Core.Semantic.Readback.Definitions
Mcltt.Core.Semantic.Readback.Lemmas
Mcltt.Core.Semantic.Realizability
Mcltt.Core.Soundness
Mcltt.Core.Soundness.ContextCases
Mcltt.Core.Soundness.FunctionCases
Mcltt.Core.Soundness.FundamentalTheorem
Mcltt.Core.Soundness.LogicalRelation
Mcltt.Core.Soundness.LogicalRelation.Core
Mcltt.Core.Soundness.LogicalRelation.CoreLemmas
Mcltt.Core.Soundness.LogicalRelation.CoreTactics
Mcltt.Core.Soundness.LogicalRelation.Definitions
Mcltt.Core.Soundness.LogicalRelation.Lemmas
Mcltt.Core.Soundness.NatCases
Mcltt.Core.Soundness.Realizability
Mcltt.Core.Soundness.SubstitutionCases
Mcltt.Core.Soundness.SubtypingCases
Mcltt.Core.Soundness.TermStructureCases
Mcltt.Core.Soundness.UniverseCases
Mcltt.Core.Soundness.Weakening
Mcltt.Core.Soundness.Weakening.Definition
Mcltt.Core.Soundness.Weakening.Lemmas
Mcltt.Core.Syntactic.CoreInversions
Mcltt.Core.Syntactic.CoreTypeInversions
Mcltt.Core.Syntactic.Corollaries
Mcltt.Core.Syntactic.CtxEq
Mcltt.Core.Syntactic.CtxSub
Mcltt.Core.Syntactic.ExpNoConfusion
Mcltt.Core.Syntactic.Presup
Mcltt.Core.Syntactic.Syntax
Concrete Syntax Tree
Abstract Syntac Tree
Syntactic Normal/Neutral Form
Syntactic Notations
Mcltt.Core.Syntactic.System
Mcltt.Core.Syntactic.System.Definitions
Mcltt.Core.Syntactic.System.Lemmas
Mcltt.Core.Syntactic.System.Tactics
Mcltt.Core.Syntactic.SystemOpt
Mcltt.Entrypoint
Mcltt.Extraction.Evaluation
Mcltt.Extraction.NbE
Mcltt.Extraction.PseudoMonadic
Mcltt.Extraction.Readback
Mcltt.Extraction.Subtyping
Mcltt.Extraction.TypeCheck
Mcltt.Frontend.Elaborator
Mcltt.Frontend.Parser
Mcltt.LibTactics