all

-- Every module of the corpus, so the whole thing can be checked in ONE
-- run: the loader deduplicates by module name, so each dependency
-- elaborates once instead of once per importer.
--
-- Since the lemma store is scoped to a module's import closure, a
-- module elaborates here exactly as it does standalone — the order of
-- the imports below does not matter, and this file subsumes the
-- per-file sweep. check-elaborations.sh verifies the list is complete.

import Lang.definingEq
import Algebra.monoid
import Algebra.group
import Algebra.groupTheory
import Algebra.subgroup
import Algebra.quotGroup
import Algebra.groupHom
import Algebra.groupIso
import Algebra.ringTheory
import Algebra.ideal
import Algebra.quotRing
import Int.ring
import Int.quot
import Algebra.field
import Natural.monoid
import Natural.algebra
import Natural.order
import Int.order
import Rat.order
import Real
import Rat.bound
import Rat.half
import Real.neg
import Real.seq
import Real.add
import Rat.arch
import Real.eq
import Real.order
import Rat.abs
import Real.abs
import Rat.lt
import Real.lt
import Real.complete
import Real.bound
import Real.mul
import Rat.invOrder
import Rat.sqrt
import Real.pos
import Real.sqrt
import Real.recip
import Algebra.ring
import Real.ring
import Real.group
import Real.metric
import Rat.max
import Real.lattice
import Natural.more
import Natural.div
import Natural.sqrt
import Rat.nat
import Rat.ceil
import Rat.floor
import Int.abs
import Int.group
import Rat.field
import Natural
import Int
import Int.normalize
import Core.equality
import Core.prop
import Core.prelude
import Natural.eq
import Int.eq
import Core.id
import Core.quotEffective
import Int.effective
import Int.add
import Int.mul
import Rat.frac
import Rat
import Rat.inv
import Int.nonZero
import Lang.letExpr
import Lang.sigmaElim
import Lang.eqElim
import Lang.sumElim
import Lang.unsquash
import Qiit.bag
import Qiit.conTy
import Qiit.cross
import Qiit.int
import Qiit.nat
import Qiit.quot
import Qiit.vec
import Lang.quotient
import Lang.quotTyUniv
import Rat.algInv
import Rat.effective
import Codata.stream
import Codata.conat
import Codata.streamEq
import Codata.streamBisim
import Core.sum
import Core.uip
import Core.bracket
import Core.propCode
import Lang.vectByInd
import Lang.vectByIndAppend