"CoreTT.AST" $ do
it "evaluates Star as VStar" $ do
evalInf empty [] Star `shouldBe` Just VStar
it "evaluates a lambda abstraction Lam b as VLam b" $ do
evalChk empty [] (Lam (Inf (Local 0))) `shouldBe` Just (VLam (Inf (Local 0)))
it "evaluates a local variable as its value in the context" $ do
evalInf empty [VStar] (Local 0) `shouldBe` Just VStar
it "raises an error when variable out of range" $ do
evalInf empty [] (Local 3) `shouldBe` Nothing
it "raises an error when we apply something not to a function" $ do
evalInf empty [] (App (Inf Star) Star) `shouldBe` Nothing
describe