summaryrefslogtreecommitdiff
path: root/Graded.lean
diff options
context:
space:
mode:
authorHannes Schulze <contact@haschu.me>2026-04-15 15:17:51 +0200
committerHannes Schulze <contact@haschu.me>2026-04-15 15:17:51 +0200
commit27ff9d5b7a21ae54aed1c7a23a23723903ab2fa9 (patch)
tree4d13dd84ac4ced2360a51799f0e5c846bd733872 /Graded.lean
parent37f7c86a7591da1233cdf1d293bf851f43c65ba1 (diff)
Revert "move wip"graded-algebra
This reverts commit 37f7c86a7591da1233cdf1d293bf851f43c65ba1.
Diffstat (limited to 'Graded.lean')
-rw-r--r--Graded.lean1
1 files changed, 1 insertions, 0 deletions
diff --git a/Graded.lean b/Graded.lean
new file mode 100644
index 0000000..39b3ce2
--- /dev/null
+++ b/Graded.lean
@@ -0,0 +1 @@
+import Graded.GradedMonad