Imports Reference

Use narrow imports while developing, and import LeanCert when you want the aggregate public API.

Direct Automation

import LeanCert.Tactic.IntervalAuto
import LeanCert.Tactic.DyadicAuto
import LeanCert.Tactic.Bound
import LeanCert.Discovery

Proof Templates

import LeanCert.Engine.Table
import LeanCert.ANT.Asymp
import LeanCert.ConstantFactory
import LeanCert.ConstantFactory.IntervalBank
import LeanCert.QProduct
import LeanCert.Analysis.ContourShift

Domain Libraries

import LeanCert.ANT
import LeanCert.Engine.ChebyshevPsi
import LeanCert.Engine.ChebyshevTheta

ML Verification

import LeanCert.ML.Network
import LeanCert.ML.Transformer
import LeanCert.ML.Optimized

Aggregate Import

import LeanCert