diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index 1e77080..0000000 --- a/lakefile.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Lake -open Lake DSL -package Qq -@[default_target] lean_lib Qq