fix build

ChrisHughes24 · May 6, 2023 · e7d4020 · e7d4020
1 parent 41a06fb
commit e7d4020
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/v1/decide.lean b/src/v1/decide.lean
@@ -1,4 +1,5 @@
 import .lemmas
+import data.fintype.pi
 
 open fintype