From 19f3c281c3921ecbe014ca4d26166ccdcbbff31c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jan 2014 16:29:32 -0800 Subject: [PATCH] test(tests/lean): matrix multiplication example Signed-off-by: Leonardo de Moura --- tests/lean/matrix.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/lean/matrix.lean diff --git a/tests/lean/matrix.lean b/tests/lean/matrix.lean new file mode 100644 index 0000000000..387df22b3f --- /dev/null +++ b/tests/lean/matrix.lean @@ -0,0 +1,18 @@ +variable matrix : Nat → Nat → Type +variable mul {m n p : Nat} : matrix n m → matrix m p → matrix n p +infixl 70 * : mul +axiom mul_assoc {m n p o : Nat} (M : matrix n m) (N : matrix m p) (P : matrix p o) : + M * (N * P) = (M * N) * P +add_rewrite mul_assoc + +-- Create an example +variable m1 : matrix 2 3 +variable m2 : matrix 3 4 +variable m3 : matrix 4 2 +variable m4 : matrix 2 6 + +(* +local t = parse_lean("m1 * (m2 * (m3 * m4))") +print("before simp: " .. tostring(t)) +print("after simp: " .. tostring(simplify(t))) +*) \ No newline at end of file