Implicit.Language.Regular.All

Implicit
- README
- Language
  - Counter2Mask
  - Base
  - Prelude
  - Bitmap
  - Shift
    - Base
    - Properties
  - Subst
    - Base
    - Properties
  - Lookup
    - Base
    - Properties
  - Occur
    - Base
    - Properties
  - Find
    - Base
    - Properties
  - Regular
    - Base
    - Properties
  - OpenClose
    - Base
  - Extension
    - Base
    - InputOutput
    - ExSol
    - Occur
    - EnvReplace
    - Properties
  - Ground
    - Base
    - Properties
  - EnvOps
    - Base
    - Inst
    - RemoveTVar
    - RemoveSVar
    - RemoveEVar
    - InsertEVar
    - InsertTVar
    - InsertUVar
    - InsertSVar
    - Regular
    - Replace
    - RemoveUVar
- Decl
  - Typing
  - Trans
  - Subtyping
  - SubtypingV2
  - Equiv
  - AuxLemmas
- Annotatability
  - Soundness
  - Corollaries
  - DeclPartial
  - IF
  - Elaboration
- Interm2Decl
- Decl2Interm
  - Corollaries
  - Main
- Algo
  - Properties
    - Regularity
    - Extension
    - Subsumption
    - Id
    - Polarity
    - Shift
    - Reflexivity
    - StrengthenTVar
    - StrengthenSVar
    - StrengthenEVar
    - Weaken
    - Irrelevance
    - Trans
    - SubIrrelevance
    - Swap
    - Subst
    - OpenK
    - WeakenEVar
    - WeakenTVar
    - WeakenSVar
  - Base
  - Constructs
    - Syntax
    - Shift
    - Subst
    - Lookup
- Algo2Interm
  - Find
  - Main
  - Corollaries
  - AlgoCounter
    - Base
    - Sound
  - Context2Counter
- Interm2Algo
  - Main
  - Corollaries
  - Counter2Context
  - ExtIrrev
  - EnvDiff
  - OpenClose
  - Find
  - AuxLemmas
  - FVClose
- Interm
  - Base
  - Properties
    - Regularity
    - Polarity
    - Extension
    - Strengthen
    - Ground

module Implicit.Language.Regular.All where

open import Implicit.Language.Regular.Base public
open import Implicit.Language.Regular.Properties public