From bfe7d1ffe88cf20a325fef88cd9e47181f08ef23 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Mar 2020 11:07:24 -0700 Subject: [PATCH] chore: add kernel WHNF test --- tests/lean/run/kernel2.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/lean/run/kernel2.lean b/tests/lean/run/kernel2.lean index eea7c549c0..d71c6af4b0 100644 --- a/tests/lean/run/kernel2.lean +++ b/tests/lean/run/kernel2.lean @@ -51,3 +51,7 @@ def c9 : String := "hello" ++ "world" def c10 : String := "helloworld" #eval checkDefEq `c9 `c10 + +def c11 : Bool := decide ('a' = 'b') + +#eval whnf `c11