Skip to content
Browse files

Lets should be in /both/ 'check' and 'synth'.

Because we want synth terms to be closed under adding a let around it.
  • Loading branch information...
1 parent 9e4c3ae commit d442bdacdcf223d83d0c34f0f3f61a57a9e35889 @mboes committed
Showing with 2 additions and 0 deletions.
  1. +2 −0 Dedukti/Runtime.hs
2 Dedukti/Runtime.hs
@@ -131,6 +131,8 @@ synth n (TApp t1 (Pair t2 c2))
synth n TType = Kind
synth n (TLam (Just (Box Type ty)) f) =
Pi ty (\xc -> synth (n + 1) (f (Pair (Box ty xc) xc)))
+synth n (TLet (Pair t tc) f)
+ | tyt <- synth n t = synth (n + 1) (f (Pair (Box tyt tc) tc))
synth n t = throw SynthError
checkDeclaration :: String -> a -> IO ()

0 comments on commit d442bda

Please sign in to comment.
Something went wrong with that request. Please try again.