Skip to content

Commit 81424e1

Browse files
committed
fix(ci): add missing imports for BitVec and SumSquares to library files
Made-with: Cursor
1 parent bd9b18d commit 81424e1

File tree

2 files changed

+2
-0
lines changed

2 files changed

+2
-0
lines changed

ToMathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ import ToMathlib.Control.OptionT
2121
import ToMathlib.Control.StateT
2222
import ToMathlib.Control.WriterT
2323
import ToMathlib.Data.ENNReal.AbsDiff
24+
import ToMathlib.Data.ENNReal.SumSquares
2425
import ToMathlib.General
2526
import ToMathlib.OrderEnrichedCategory
2627
import ToMathlib.PFunctor.Basic

VCVio.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ import VCVio.EvalDist.Prod
3434
import VCVio.EvalDist.TVDist
3535
import VCVio.OracleComp.Coercions.Add
3636
import VCVio.OracleComp.Coercions.SubSpec
37+
import VCVio.OracleComp.Constructions.BitVec
3738
import VCVio.OracleComp.Constructions.GenerateSeed
3839
import VCVio.OracleComp.Constructions.Replicate
3940
import VCVio.OracleComp.Constructions.SampleableType

0 commit comments

Comments
 (0)