Mcltt Algorithmic Algorithmic Algorithmic/Subtyping Subtyping Algorithmic/Typing Typing Core Core Core/Completeness Completeness Core/Completeness/Consequences Consequences Core/Completeness/LogicalRelation LogicalRelation Core/Semantic Semantic Core/Semantic/Evaluation Evaluation Core/Semantic/PER PER Core/Semantic/Readback Readback Core/Soundness Soundness Core/Soundness/LogicalRelation LogicalRelation Core/Soundness/Weakening Weakening Core/Syntactic Syntactic Core/Syntactic/System System Extraction Extraction Frontend Frontend Mcltt.Algorithmic.Subtyping.Definitions Definitions Mcltt.Algorithmic.Subtyping.Lemmas Lemmas Mcltt.Algorithmic.Subtyping.Definitions->Mcltt.Algorithmic.Subtyping.Lemmas Mcltt.Algorithmic.Typing.Definitions Definitions Mcltt.Algorithmic.Subtyping.Definitions->Mcltt.Algorithmic.Typing.Definitions Mcltt.Algorithmic.Typing.Lemmas Lemmas Mcltt.Algorithmic.Subtyping.Lemmas->Mcltt.Algorithmic.Typing.Lemmas Mcltt.Algorithmic.Subtyping Subtyping Mcltt.Algorithmic.Subtyping.Lemmas->Mcltt.Algorithmic.Subtyping Mcltt.Algorithmic.Typing.Definitions->Mcltt.Algorithmic.Typing.Lemmas Mcltt.Algorithmic.Typing Typing Mcltt.Algorithmic.Typing.Lemmas->Mcltt.Algorithmic.Typing Mcltt.Extraction.Subtyping Subtyping Mcltt.Algorithmic.Subtyping->Mcltt.Extraction.Subtyping Mcltt.Extraction.TypeCheck TypeCheck Mcltt.Algorithmic.Typing->Mcltt.Extraction.TypeCheck Mcltt.Core.Completeness.Consequences.Rules Rules Mcltt.Core.Completeness.Consequences.Rules->Mcltt.Algorithmic.Subtyping.Lemmas Mcltt.Core.Completeness.Consequences.Types Types Mcltt.Core.Semantic.Consequences Consequences Mcltt.Core.Completeness.Consequences.Types->Mcltt.Core.Semantic.Consequences Mcltt.Core.Completeness.LogicalRelation.Definitions Definitions Mcltt.Core.Completeness.LogicalRelation.Lemmas Lemmas Mcltt.Core.Completeness.LogicalRelation.Definitions->Mcltt.Core.Completeness.LogicalRelation.Lemmas Mcltt.Core.Completeness.LogicalRelation LogicalRelation Mcltt.Core.Completeness.LogicalRelation.Lemmas->Mcltt.Core.Completeness.LogicalRelation Mcltt.Core.Completeness.LogicalRelation.Tactics Tactics Mcltt.Core.Completeness.LogicalRelation.Tactics->Mcltt.Core.Completeness.LogicalRelation.Lemmas Mcltt.Core.Completeness Completeness Mcltt.Core.Completeness->Mcltt.Core.Completeness.Consequences.Rules Mcltt.Core.Completeness->Mcltt.Core.Completeness.Consequences.Types Mcltt.Core.Completeness.FundamentalTheorem FundamentalTheorem Mcltt.Core.Completeness.FundamentalTheorem->Mcltt.Core.Completeness Mcltt.Core.Soundness.LogicalRelation.Lemmas Lemmas Mcltt.Core.Completeness.FundamentalTheorem->Mcltt.Core.Soundness.LogicalRelation.Lemmas Mcltt.Core.Completeness.ContextCases ContextCases Mcltt.Core.Completeness.SubstitutionCases SubstitutionCases Mcltt.Core.Completeness.ContextCases->Mcltt.Core.Completeness.SubstitutionCases Mcltt.Core.Completeness.UniverseCases UniverseCases Mcltt.Core.Completeness.LogicalRelation->Mcltt.Core.Completeness.UniverseCases Mcltt.Core.Completeness.VariableCases VariableCases Mcltt.Core.Completeness.LogicalRelation->Mcltt.Core.Completeness.VariableCases Mcltt.Core.Completeness.UniverseCases->Mcltt.Core.Completeness.ContextCases Mcltt.Core.Completeness.TermStructureCases TermStructureCases Mcltt.Core.Completeness.UniverseCases->Mcltt.Core.Completeness.TermStructureCases Mcltt.Core.Completeness.FunctionCases FunctionCases Mcltt.Core.Completeness.SubtypingCases SubtypingCases Mcltt.Core.Completeness.FunctionCases->Mcltt.Core.Completeness.SubtypingCases Mcltt.Core.Completeness.TermStructureCases->Mcltt.Core.Completeness.FunctionCases Mcltt.Core.Completeness.NatCases NatCases Mcltt.Core.Completeness.TermStructureCases->Mcltt.Core.Completeness.NatCases Mcltt.Core.Completeness.NatCases->Mcltt.Core.Completeness.FundamentalTheorem Mcltt.Core.Completeness.SubstitutionCases->Mcltt.Core.Completeness.NatCases Mcltt.Core.Completeness.VariableCases->Mcltt.Core.Completeness.FundamentalTheorem Mcltt.Core.Completeness.SubtypingCases->Mcltt.Core.Completeness.FundamentalTheorem Mcltt.Core.Semantic.Consequences->Mcltt.Algorithmic.Typing.Lemmas Mcltt.Core.Semantic.Evaluation.Definitions Definitions Mcltt.Core.Semantic.Evaluation.Lemmas Lemmas Mcltt.Core.Semantic.Evaluation.Definitions->Mcltt.Core.Semantic.Evaluation.Lemmas Mcltt.Core.Semantic.Evaluation.Tactics Tactics Mcltt.Core.Semantic.Evaluation.Lemmas->Mcltt.Core.Semantic.Evaluation.Tactics Mcltt.Core.Semantic.Evaluation Evaluation Mcltt.Core.Semantic.Evaluation.Tactics->Mcltt.Core.Semantic.Evaluation Mcltt.Core.Semantic.PER.CoreTactics CoreTactics Mcltt.Core.Semantic.PER.Lemmas Lemmas Mcltt.Core.Semantic.PER.CoreTactics->Mcltt.Core.Semantic.PER.Lemmas Mcltt.Core.Semantic.PER.Definitions Definitions Mcltt.Core.Semantic.PER.Definitions->Mcltt.Core.Semantic.PER.CoreTactics Mcltt.Core.Semantic.PER PER Mcltt.Core.Semantic.PER.Lemmas->Mcltt.Core.Semantic.PER Mcltt.Core.Semantic.Readback.Definitions Definitions Mcltt.Core.Semantic.Readback.Lemmas Lemmas Mcltt.Core.Semantic.Readback.Definitions->Mcltt.Core.Semantic.Readback.Lemmas Mcltt.Core.Semantic.Readback Readback Mcltt.Core.Semantic.Readback.Lemmas->Mcltt.Core.Semantic.Readback Mcltt.Core.Semantic.NbE NbE Mcltt.Core.Semantic.NbE->Mcltt.Algorithmic.Subtyping.Definitions Mcltt.Core.Semantic.Realizability Realizability Mcltt.Core.Semantic.NbE->Mcltt.Core.Semantic.Realizability Mcltt.Extraction.NbE NbE Mcltt.Core.Semantic.NbE->Mcltt.Extraction.NbE Mcltt.Core.Semantic.Realizability->Mcltt.Core.Completeness.NatCases Mcltt.Core.Soundness.Realizability Realizability Mcltt.Core.Semantic.Realizability->Mcltt.Core.Soundness.Realizability Mcltt.Core.Semantic.PER->Mcltt.Core.Completeness.LogicalRelation.Definitions Mcltt.Core.Semantic.PER->Mcltt.Core.Completeness.LogicalRelation.Tactics Mcltt.Core.Semantic.PER->Mcltt.Core.Semantic.Realizability Mcltt.Core.Soundness.LogicalRelation.Definitions Definitions Mcltt.Core.Semantic.PER->Mcltt.Core.Soundness.LogicalRelation.Definitions Mcltt.Core.Semantic.Domain Domain Mcltt.Core.Semantic.Domain->Mcltt.Core.Semantic.Evaluation.Definitions Mcltt.Core.Semantic.Evaluation->Mcltt.Core.Semantic.Readback.Definitions Mcltt.Extraction.Evaluation Evaluation Mcltt.Core.Semantic.Evaluation->Mcltt.Extraction.Evaluation Mcltt.Core.Semantic.Readback->Mcltt.Core.Semantic.PER.Definitions Mcltt.Core.Semantic.Readback->Mcltt.Core.Semantic.NbE Mcltt.Extraction.Readback Readback Mcltt.Core.Semantic.Readback->Mcltt.Extraction.Readback Mcltt.Core.Soundness.LogicalRelation.Core Core Mcltt.Core.Soundness.LogicalRelation.Core->Mcltt.Core.Soundness.Realizability Mcltt.Core.Soundness.LogicalRelation LogicalRelation Mcltt.Core.Soundness.LogicalRelation.Lemmas->Mcltt.Core.Soundness.LogicalRelation Mcltt.Core.Soundness.LogicalRelation.CoreLemmas CoreLemmas Mcltt.Core.Soundness.LogicalRelation.CoreLemmas->Mcltt.Core.Soundness.LogicalRelation.Core Mcltt.Core.Soundness.LogicalRelation.CoreTactics CoreTactics Mcltt.Core.Soundness.LogicalRelation.CoreTactics->Mcltt.Core.Soundness.LogicalRelation.CoreLemmas Mcltt.Core.Soundness.LogicalRelation.Definitions->Mcltt.Core.Soundness.LogicalRelation.CoreTactics Mcltt.Core.Soundness.Weakening.Lemmas Lemmas Mcltt.Core.Soundness.Weakening.Lemmas->Mcltt.Core.Soundness.LogicalRelation.CoreLemmas Mcltt.Core.Soundness.Weakening Weakening Mcltt.Core.Soundness.Weakening.Lemmas->Mcltt.Core.Soundness.Weakening Mcltt.Core.Soundness.Weakening.Definitions Definitions Mcltt.Core.Soundness.Weakening.Definitions->Mcltt.Core.Soundness.LogicalRelation.Definitions Mcltt.Core.Soundness.Weakening.Definitions->Mcltt.Core.Soundness.Weakening.Lemmas Mcltt.Core.Soundness Soundness Mcltt.Core.Soundness->Mcltt.Algorithmic.Subtyping.Lemmas Mcltt.Core.Soundness->Mcltt.Core.Semantic.Consequences Mcltt.Core.Soundness.FundamentalTheorem FundamentalTheorem Mcltt.Core.Soundness.FundamentalTheorem->Mcltt.Core.Soundness Mcltt.Core.Soundness.ContextCases ContextCases Mcltt.Core.Soundness.FunctionCases FunctionCases Mcltt.Core.Soundness.ContextCases->Mcltt.Core.Soundness.FunctionCases Mcltt.Core.Soundness.NatCases NatCases Mcltt.Core.Soundness.ContextCases->Mcltt.Core.Soundness.NatCases Mcltt.Core.Soundness.LogicalRelation->Mcltt.Core.Soundness.ContextCases Mcltt.Core.Soundness.SubtypingCases SubtypingCases Mcltt.Core.Soundness.LogicalRelation->Mcltt.Core.Soundness.SubtypingCases Mcltt.Core.Soundness.TermStructureCases TermStructureCases Mcltt.Core.Soundness.LogicalRelation->Mcltt.Core.Soundness.TermStructureCases Mcltt.Core.Soundness.FunctionCases->Mcltt.Core.Soundness.FundamentalTheorem Mcltt.Core.Soundness.SubstitutionCases SubstitutionCases Mcltt.Core.Soundness.SubstitutionCases->Mcltt.Core.Soundness.FunctionCases Mcltt.Core.Soundness.SubstitutionCases->Mcltt.Core.Soundness.NatCases Mcltt.Core.Soundness.UniverseCases UniverseCases Mcltt.Core.Soundness.SubtypingCases->Mcltt.Core.Soundness.UniverseCases Mcltt.Core.Soundness.TermStructureCases->Mcltt.Core.Soundness.UniverseCases Mcltt.Core.Soundness.UniverseCases->Mcltt.Core.Soundness.SubstitutionCases Mcltt.Core.Soundness.NatCases->Mcltt.Core.Soundness.FundamentalTheorem Mcltt.Core.Soundness.Realizability->Mcltt.Core.Soundness.LogicalRelation.Lemmas Mcltt.Core.Syntactic.System.Definitions Definitions Mcltt.Core.Syntactic.System.Lemmas Lemmas Mcltt.Core.Syntactic.System.Definitions->Mcltt.Core.Syntactic.System.Lemmas Mcltt.Core.Syntactic.System.Tactics Tactics Mcltt.Core.Syntactic.System.Lemmas->Mcltt.Core.Syntactic.System.Tactics Mcltt.Core.Syntactic.System System Mcltt.Core.Syntactic.System.Tactics->Mcltt.Core.Syntactic.System Mcltt.Core.Syntactic.SystemOpt SystemOpt Mcltt.Core.Syntactic.SystemOpt->Mcltt.Algorithmic.Subtyping.Definitions Mcltt.Core.Syntactic.SystemOpt->Mcltt.Core.Completeness.VariableCases Mcltt.Core.Syntactic.SystemOpt->Mcltt.Core.Soundness.Weakening.Definitions Mcltt.Core.Syntactic.CoreInversions CoreInversions Mcltt.Core.Syntactic.SystemOpt->Mcltt.Core.Syntactic.CoreInversions Mcltt.Core.Syntactic.CoreInversions->Mcltt.Core.Completeness.Consequences.Types Mcltt.Core.Syntactic.Corollaries Corollaries Mcltt.Core.Syntactic.CoreInversions->Mcltt.Core.Syntactic.Corollaries Mcltt.Core.Syntactic.Syntax Syntax Mcltt.Core.Syntactic.Syntax->Mcltt.Core.Semantic.Domain Mcltt.Core.Syntactic.Syntax->Mcltt.Core.Syntactic.System.Definitions Mcltt.Frontend.Elaborator Elaborator Mcltt.Core.Syntactic.Syntax->Mcltt.Frontend.Elaborator Mcltt.Frontend.Parser Parser Mcltt.Core.Syntactic.Syntax->Mcltt.Frontend.Parser Mcltt.Core.Syntactic.System->Mcltt.Core.Semantic.NbE Mcltt.Core.Syntactic.CoreTypeInversions CoreTypeInversions Mcltt.Core.Syntactic.System->Mcltt.Core.Syntactic.CoreTypeInversions Mcltt.Core.Syntactic.CtxSub CtxSub Mcltt.Core.Syntactic.System->Mcltt.Core.Syntactic.CtxSub Mcltt.Core.Syntactic.Corollaries->Mcltt.Core.Soundness.Weakening.Lemmas Mcltt.Core.Syntactic.CoreTypeInversions->Mcltt.Core.Syntactic.SystemOpt Mcltt.Core.Syntactic.CtxEq CtxEq Mcltt.Core.Syntactic.Presup Presup Mcltt.Core.Syntactic.CtxEq->Mcltt.Core.Syntactic.Presup Mcltt.Core.Syntactic.CtxSub->Mcltt.Core.Syntactic.CtxEq Mcltt.Core.Syntactic.Presup->Mcltt.Core.Syntactic.SystemOpt Mcltt.Core.Base Base Mcltt.Core.Base->Mcltt.Core.Syntactic.Syntax Mcltt.Extraction.NbE->Mcltt.Extraction.Subtyping Mcltt.Entrypoint Entrypoint Mcltt.Extraction.TypeCheck->Mcltt.Entrypoint Mcltt.Extraction.Evaluation->Mcltt.Extraction.Readback Mcltt.Extraction.Readback->Mcltt.Extraction.NbE Mcltt.Extraction.PseudoMonadic PseudoMonadic Mcltt.Extraction.PseudoMonadic->Mcltt.Extraction.Subtyping Mcltt.Extraction.Subtyping->Mcltt.Extraction.TypeCheck Mcltt.Frontend.Elaborator->Mcltt.Algorithmic.Typing.Lemmas Mcltt.Frontend.Parser->Mcltt.Entrypoint Mcltt.LibTactics LibTactics Mcltt.LibTactics->Mcltt.Core.Semantic.Evaluation.Lemmas Mcltt.LibTactics->Mcltt.Core.Syntactic.System.Definitions Mcltt.LibTactics->Mcltt.Frontend.Elaborator