Fsub.Base.Label
Fsub.Base.LabelMap
Fsub.Base.Tactics
Fsub.Base.Fsub_LetSum_Definitions
- Syntax (pre-terms)
- Concrete Qualifiers
- Opening terms
- Local closure
- Environments
- Well-formedness
- Subtyping
- Typing
- Values
- Reduction
- Automation
Fsub.Base.Fsub_LetSum_Infrastructure
- Free variables
- Substitution
- The "gather_atoms" tactic
- Properties of opening and substitution
- Local closure is preserved under substitution
- Properties of body_e
- Automation
Fsub.Base.Fsub_LetSum_Lemmas
- Properties of wf_typ
- Properties of wf_env and wf_typ
- Properties of wf_env
- Environment is unchanged by substitution for a fresh name
- Regularity of relations
- Automation
Fsub.Base.Fsub_LetSum_Soundness
Fsub.ExtendedBase.Label
Fsub.ExtendedBase.Lattice
Fsub.ExtendedBase.LabelMap
Fsub.ExtendedBase.Tactics
Fsub.ExtendedBase.Fsub_LetSum_Definitions
- Syntax (pre-terms)
- Concrete Qualifiers
- Opening terms
- Local closure
- Environments
- Well-formedness
- Subtyping
- Typing
- Values
- Reduction
- Automation
Fsub.ExtendedBase.Fsub_LetSum_Infrastructure
- Free variables
- Substitution
- The "gather_atoms" tactic
- Properties of opening and substitution
- Local closure is preserved under substitution
- Properties of body_e
- Automation
Fsub.ExtendedBase.Fsub_LetSum_Lemmas
- Properties of wf_typ
- Properties of wf_env and wf_typ
- Properties of wf_env
- Environment is unchanged by substitution for a fresh name
- Regularity of relations
- Automation
Fsub.ExtendedBase.Fsub_LetSum_Soundness
Fsub.CaptureTrack.Label
Fsub.CaptureTrack.LabelMap
Fsub.CaptureTrack.Tactics
Fsub.CaptureTrack.Fsub_LetSum_Definitions
- Syntax (pre-terms)
- Concrete Qualifiers
- Opening terms
- Local closure
- Environments
- Well-formedness
- Subtyping
- Typing
- Values
- Reduction
- Automation
Fsub.CaptureTrack.Fsub_LetSum_Infrastructure
- Free variables
- Substitution
- The "gather_atoms" tactic
- Properties of opening and substitution
- Local closure is preserved under substitution
- Properties of body_e
- Automation
Fsub.CaptureTrack.Fsub_LetSum_Lemmas
- Properties of wf_typ
- Properties of wf_env and wf_typ
- Properties of wf_env
- Environment is unchanged by substitution for a fresh name
- Regularity of relations
- Automation
Fsub.CaptureTrack.Fsub_LetSum_Soundness
Fsub.FuncColour.Label
Fsub.FuncColour.LabelMap
Fsub.FuncColour.Tactics
Fsub.FuncColour.Fsub_LetSum_Definitions
- Syntax (pre-terms)
- Concrete Qualifiers
- Opening terms
- Local closure
- Environments
- Well-formedness
- Subtyping
- Typing
- Values
- Reduction
- Automation
Fsub.FuncColour.Fsub_LetSum_Infrastructure
- Free variables
- Substitution
- The "gather_atoms" tactic
- Properties of opening and substitution
- Local closure is preserved under substitution
- Properties of body_e
- Automation
Fsub.FuncColour.Fsub_LetSum_Lemmas
- Properties of wf_typ
- Properties of wf_env and wf_typ
- Properties of wf_env
- Environment is unchanged by substitution for a fresh name
- Regularity of relations
- Automation
Fsub.FuncColour.Fsub_LetSum_Soundness
Fsub.RefImmut.Label
Fsub.RefImmut.LabelMap
Fsub.RefImmut.Tactics
Fsub.RefImmut.Signatures
Fsub.RefImmut.Fsub_LetSum_Definitions
- Syntax (pre-terms)
- Concrete Qualifiers
- Opening terms
- Local closure
- Environments
- Well-formedness
- Subtyping
- Typing
- Values
- Stores
- Reduction
- Automation
Fsub.RefImmut.Fsub_LetSum_Infrastructure
- Free variables
- Substitution
- The "gather_atoms" tactic
- Properties of opening and substitution
- Local closure is preserved under substitution
- Properties of body_e
- Automation
Fsub.RefImmut.Fsub_LetSum_Lemmas
- Properties of wf_typ
- Properties of wf_env and wf_typ
- Properties of wf_env
- Environment is unchanged by substitution for a fresh name
- Regularity of relations
- Automation
Fsub.RefImmut.Fsub_LetSum_Soundness
Fsub.FqMeta.AssocList
- Implementation
- Basic definitions
- List properties
- Properties of map and dom
- The simpl_alist tactic
- The rewrite_alist tactic
- Induction
- Basic facts about disjoint
- Basic facts about uniq
- Basic facts about binds
- Hints
- List properties
- Tactic support for disjoint and uniq
- Facts about uniq
- Tactic support for binds
- Facts about binds
- Hints
Fsub.FqMeta.CoqEqDec
Fsub.FqMeta.CoqFSetDecide
Fsub.FqMeta.CoqFSetInterface
Fsub.FqMeta.CoqListFacts
Fsub.FqMeta.CoqUniquenessTac
Fsub.FqMeta.CoqUniquenessTacEx
Fsub.FqMeta.FSetExtra
Fsub.FqMeta.FSetWeakNotin
- Implementation
- Facts about set non-membership
- Hints
- Tactics for non-membership
- Examples and test cases
Fsub.FqMeta.LibDefaultSimp
Fsub.FqMeta.LibLNgen
Fsub.FqMeta.LibTactics
- Variations on built-in tactics
- Delineating cases in proofs
- Tactics for working with lists and proof contexts
Fsub.FqMeta.Metatheory
- Notations for finite sets of atoms
- Environments
- Cofinite quantification
- Lemma aliases
- Hints
- Decidable equality
- Ott compatibility