From 62651f13e08304d8fa6395fde7352984f48adb46 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 5 Nov 2025 09:09:53 +0100 Subject: evaluate deBruijn terms in environment --- lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs') diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs index cff047d..85c9d6b 100644 --- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs +++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs @@ -1,7 +1,7 @@ {-# LANGUAGE TypeApplications #-} module Minilang.Lambda.DeBruijnSpec where -import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn) +import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn, eval') import qualified Minilang.Lambda.Eval as Eval import Test.Hspec (Spec, it, shouldBe) import Data.Text (Text) @@ -18,3 +18,8 @@ spec = do let term = App (App (Lam "x" (Lam "y" (Var "x" 1))) (FV "z")) (FV "t") eval @Text term `shouldBe` FV "z" + + it "evaluates deBruijn term in env" $ do + let term = App (FV "z") (FV "t") + env = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))] + eval' @Text env term `shouldBe` FV "t" -- cgit v1.3.1