From 2cbf0ba8e97fd340b27c9133bd1ce7ae71d7e994 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Sep 2021 12:58:22 -0700 Subject: [PATCH] test: add "parameters" that are fixed in all equations --- tests/lean/run/structuralEqns.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tests/lean/run/structuralEqns.lean b/tests/lean/run/structuralEqns.lean index 11844e75b5..e1a60763bd 100644 --- a/tests/lean/run/structuralEqns.lean +++ b/tests/lean/run/structuralEqns.lean @@ -65,3 +65,17 @@ def r (i j : Nat) : Nat := #check r.eq_1 #check r.eq_2 #check r.eq_3 + +def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α := + f i <| + match j with + | Nat.zero => i + | Nat.succ j => + g i <| match j with + | Nat.zero => a + | Nat.succ j => bla f g a i j + +#eval tst ``bla +#check @bla.eq_1 +#check @bla.eq_2 +#check @bla.eq_3