Permalink
Browse files

Whoops, should check compile.

  • Loading branch information...
1 parent 234332d commit 54511dd2a4e689b6ff997faa5979306f4ffae0ac @luqui committed Feb 18, 2009
Showing with 2 additions and 1 deletion.
  1. +2 −1 experiments/icl.hs
View
@@ -22,6 +22,7 @@ data Term
| Term :% Term
| L
| G
+ deriving (Show)
-- This first section implements Aβη. (==) is β-equality.
instance Eq Term where
@@ -89,7 +90,7 @@ withNeutral rng f = do
local (Map.insert n rng) $ f (Neutral n)
prove :: Term -> Proof ()
-prove t = go . rwhnf
+prove = go . rwhnf
where
go (G :% x :% y :% z) = do -- rule Gi
prove (L :% x)

0 comments on commit 54511dd

Please sign in to comment.