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