max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add kernel WHNF test

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-18 11:07:24 -07:00
parent 6f62986368
commit bfe7d1ffe8
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/kernel2.lean
View file

@ -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