1 files changed, 39 insertions, 0 deletions
diff --git a/units.lisp b/units.lisp
new file mode 100644
index 0000000..4b353e1
--- /dev/null
+++ b/units.lisp
@@ -0,0 +1,39 @@
+(defun m (x)
+  x)
+
+(defun s (x)
+  x)
+
+(defthm m+m
+  (equal (+ (m x) (m y))
+         (m (+ x y))))
+
+(defthm s+s
+  (equal (+ (s x) (s y))
+         (s (+ x y))))
+
+(defun m/s (x)
+  x)
+
+(defthm m/s+m/s
+  (equal (+ (m/s x) (m/s y))
+         (m/s (+ x y))))
+
+(defthm m/s*s
+  (equal (* (m/s x) (s y))
+         (m (* x y))))
+
+(defthm m*/s
+  (equal (* (m x) (/ (s y)))
+         (m/s (* x (/ y)))))
+
+(defthm m*/m/s
+  (equal (* (m x) (/ (m/s y)))
+         (m (* x (/ y)))))
+
+(in-theory (disable m s m/s))
+
+(defthm test
+  (equal (/ (m x) (/ (m y) (s z)))
+         (m (/ x (/ y z))))
+  :rule-classes nil)