Agda.Compiler.Epic.Smashing
Description
Smash functions which return something that can be inferred (something of a type with only one element)
Documentation
inferable :: Set QName -> QName -> [Arg Term] -> Compile TCM (Maybe Expr)
Can a datatype be inferred? If so, return the only possible value.
smashable :: Int -> Type -> Compile TCM (Maybe Expr)
Find the only possible value for a certain type. If we fail return Nothing
buildLambda :: (Ord n, Num n) => n -> Expr -> Expr