Core.lean

import Core.Types
import Core.SepRange
import Core.FrameRecords
import Core.World
import Core.ShapeMu
import Core.Images
import Core.Invariant
import Core.Wp
import Core.Relation
import Core.RelMu
import Core.RelationFacts
import Core.ReborrowShapes
import Core.Reborrow
import Core.FrameRules
import Core.EffWp
import Core.DivDefs
import Core.DivWp
import Core.DivRules
import Core.DivIterate
import Core.DivHandlers
import Core.DivFuel
import Core.DivReify
import Core.DivHandle
import Core.DivHandleLast
import Core.DivPrograms
import Core.DivRuntime
import Core.DivDrive
import Core.HandleLastErase
import Core.EffCancel
import Core.EffCancelTyped
import Core.Persistent
import Core.Compatibility
import Core.NuRel
import Core.Computation
import Core.Compat
import Core.EffRules
import Core.EffBorrow
import Core.EffBoxed
import Core.Sized
import Core.FoldImm
import Core.FoldOwn
import Core.FoldReuse
import Core.FoldOwnG
import Core.FoldOwnGTerm
import Core.FoldClass
import Core.Nu
import Core.CapNorm
import Core.CodeNu
import Core.CodeRules
import Core.CodeNuOut
import Core.Alpha
import Core.Fundamental
import Core.Examples
import Core.Embedding
import Core.EmbeddingExamples
import Core.Fix
import Core.Lists
import Core.Count
import Core.CountFree
import Core.MapMut
import Core.Folds
import Core.Blocks
import Core.CommonList
import Core.Records
import Core.Splits
import Core.RecordPrograms
import Core.Family
import Core.FamilyPrograms
import Core.Weaken
import Core.BlockBorrow
import Core.BlockTrack
import Core.BlockPrograms
import Core.ReuseList
import Core.DelayApprox
import Core.DelayPrograms
import Core.Steps
import Core.Closed
import Core.Run
import Core.EffMachine
import Core.DelayNaive
import Core.StreamPrograms
import Core.Integers
import Core.IntPrograms
import Core.Consume
import Core.Classes
import Core.Tok
import Core.Decl
import Core.DeclLend
import Core.ArrayWp
import Core.Arrays
import Core.SliceFrames
import Core.Slices
import Core.CountFold
import Core.ArrayPrograms
import Core.NestedPrograms
import Core.Demonic
import Core.EffExamples
import Core.EffPrograms
import Core.Totality
import Core.EffSafety
import Core.Tied
import Core.InsertDead
import Core.PinDerives
import Core.PinLaw
import Core.PinFundamental
import Core.AwaitCancel
import Core.LetCopy
import Core.RaiseNames
import Core.EffCancelRuns
import Core.Inversions
import Core.Rejections
import Core.EffTier1Programs
import Core.Stale
import Core.Stdio
import Core.Handlers
import Core.ClauseKinds
import Core.ClauseNames
import Core.HandledNames
import Core.ClauseOwn
import Core.Clo
import Core.CloRules
import Core.CloPrograms
import Core.NuBorrow
import Core.NuBorrowPrograms
import Core.Mentions
import Core.ResourceSafety
import Core.StepsN
import Core.TreeWp
import Core.TreeWpEff
import Core.TreeSem
import Core.TreeSemC
import Core.TreeSemK
import Core.TreeSemKEx
import Core.TreeSemObs
import Core.TreeCactus
import Core.TreeStepKeep
import Core.TreeHeadlines
import Core.TreeHeap
import Core.TreeHandle
import Core.TreeSched
import Core.TreeSchedProgs
import Core.TreeResume
import Core.TreePool
import Core.TreeLend
import Core.TreeSchedPool
import Core.TreeLendJoin
import Core.TreeBorrowEdges
import Core.TreeConsume
import Core.TreeConsumeInst
import Core.TreeSchedRelay
import Core.TreePoolSched
import Core.TreePoolSchedProgs
import Core.TreePoolSpawn
import Core.TreePoolSpawnProgs
import Core.TreePoolShare
import Core.TreePoolJoinProgs
import Core.TreeGoal791
import Core.Chain