From 672a889c83cfc00a07a78a28a9d9d99ae1a41162 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Mar 2022 09:15:43 -0700 Subject: [PATCH] test: add hlist pattern match example --- tests/lean/run/hlistOverload.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/tests/lean/run/hlistOverload.lean b/tests/lean/run/hlistOverload.lean index 5fc33715d4..f32e49e974 100644 --- a/tests/lean/run/hlistOverload.lean +++ b/tests/lean/run/hlistOverload.lean @@ -34,3 +34,17 @@ example : [10, true, 20.1].nth #2 = 20.1 := rfl #eval [10, true, 20.1].nth #0 #eval [10, true, 20.1].nth #1 #eval [10, true, 20.1].nth #2 + +def HListPatternMatch (l : HList [Nat, String]) := + match l with + | [1, "2"] => true + | [2, "1"] => true + | _ => false + +#eval HListPatternMatch [1, "2"] +#eval HListPatternMatch [2, "1"] +#eval HListPatternMatch [3, "1"] + +example : HListPatternMatch [1, "2"] := rfl +example : HListPatternMatch [2, "1"] := rfl +example : !HListPatternMatch [3, "1"] := rfl