Skip to content

Commit fdceae0

Browse files
committed
fix fix
1 parent 554ad49 commit fdceae0

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Foundation.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -516,6 +516,7 @@ public import Foundation.Vorspiel.Nat.Matrix
516516
public import Foundation.Vorspiel.NotationClass
517517
public import Foundation.Vorspiel.Option
518518
public import Foundation.Vorspiel.Order
519+
public import Foundation.Vorspiel.Part
519520
public import Foundation.Vorspiel.Preorder
520521
public import Foundation.Vorspiel.Quotient
521522
public import Foundation.Vorspiel.Rel.Basic

0 commit comments

Comments
 (0)