Library ASCommon.Common

• Utility functions
• Finite decidable quantifiers
• Finite number utilities

Library ASCommon.CBase

• Default Typeclass opaque
• Axioms
  • Make functional extensionality work with rewriting
• Notations
• Operator typeclasses
• Utility functions
• Cartesian product
• Constrained quantifiers
• Relations
• Ltac2 utilities
  • Ltac2 debug printers
    • Ltac2 inductive type manipulation
    • Ltac2 goal printer
• Conversion check
• Tactic options
• Utility tactics
  • Hypothesis management
  • Rewriting
  • Typeclass clean
  • Destruct decide
  • Evar blocking
• Proof search
• Typeclass magic
• Record management and lenses
  • Getter and setter vertical composition
  • Getter and setter horizontal merging
  • Constants getter
  • Record equality unfolding
• Pair management
• EmptyT and DecisionT
  • Inhabited, EmptyT, and DecisionT, missing base type instances
• Identity Monad
• Computable transport
  • Computable transport combinators
  • Computable transport for fin

Library ASCommon.CExtraction

• Base defaults
• Bools
• Integers
• Strings
• Lists
• Finite numbers
• Vector
• HVec
• Result
• CTrans

Library ASCommon.Options

Library ASCommon.CSimp

• User configuration
• Tactic internals
  • Leaf rewriting rule search
  • Helper lemmas
  • Main tactic body
• Default rewriting rules
  • Pair rewriting

Library ASCommon.CDestruct

• Injectivity
• ObvFalse
  • Incompatible
• ObvTrue
• CDestruct
  • CDestruct options
  • CDestruct helper tactics
    • Breaking up match cases
    • Substitution
    • Blocking
  • CDestruct Step
  • CDestruct top-level setup and syntax
    • Preprocessing tactics
• Default Instanciation of the CDestruct typeclass options
  • Inductive case splitting
  • Match case splitting
  • ObvFalse simplification
  • Injectivity
  • Substitution
  • CTrans simplification and substitution
  • JMeq simplification
  • bool_decide simplification
  • Logical connectives simplification
  • Set handling

Library ASCommon.CArith

• Decision instances
• Integer lattice
• N and nat unfolding typeclasses
• fin utils
• FinUnfold
• Arithemetic simplification

Library ASCommon.CList

• List simplification
  • Csimp instances
• List lookup with different keys
• List lookup unfold
• List boolean unfolding
• Decisions
• List utility functions
  • seqN
  • seqZ
  • List and option inversion
• List lemmas
  • Forall2 Lemmas
  • fold_left invariant proofs
• Fmap Unfold
• NoDup management
• InT
• List as monad
• sublist

Library ASCommon.CVec

• Vector alter
• Vector partial lookup
• Vector heterogenous equality
• Vector transport
• Vector countable
• cprodn
• vmapM
• vimap
• venumerate

Library ASCommon.COption

• EqSomeUnfold
• EqNoneUnfold
• CDestrEqSome
• CDestrSimpl
• Hint database for options
• Option are a monad

Library ASCommon.CBool

• Bool unfold
• Decidable propositions
• Equality decision
  • Dependent equality decision
  • Record equality decision
  • Decision of record of propositions
  • Hint database to decide equality

Library ASCommon.CBitvector

• Computable transport instance
• Rewrite databases
• bv_solve improvements
• Extra bitvector functions
• Extra bvn functions

Library ASCommon.CInduction

Library ASCommon.CMaps

• Map utilities
• Lookup Unfold
• Lookup Total Unfold
• Map related Set unfoldings
• Map induction
• FinMap reduce
• FinMap setter
• DMap : Dependant map
  • DMap methods
  • DMap lemmas
• Pretty printing maps

Library ASCommon.CSets

• Utilities
• Simplification
• Set Unfolding
• Set Induction

Library ASCommon.CMonads

• Generic monad lift
• Generic correctness typeclasses
• Monad iterators

Library ASCommon.GRel

• Maps of sets utilities
• Grels
  • Domain and range
  • Sequence
  • Inversion
  • Set into rel
  • Transitive closure

Library ASCommon.CResult

• CDestruct interaction
• Result as monad
• Error map

Library ASCommon.StateT

• Definitions
• Monad laws and properties

Library ASCommon.Effects

• Base effect definitions
• Sub-Effects and effect conversion
• Effect typeclasses
  • Effect wellformedness
  • Effect transportability
• Effect sums
• Non determinism effect: MChoice
  • MChoice helper functions
• State effect: MState
  • MState helper functions

Library ASCommon.FMon

• Free monad
• Events
• Event as transitions
  • Replay function
  • Free monad traces
    • Trace ends
    • Traces
    • Full traces
  • Free monad effect handling
• Choice monad: Non deterministic free monad
  • Matching a choice monad with a trace that does not contain choice
  • Choice monad equivalence

Library ASCommon.Exec

• Base execution result definitions
• Base execution monad definitions
• Unfold typeclass for execution results
  • Actual unfolding lemmas
• Unfold the has_error predicate

Library ASCommon.HVec