Agda-2.3.0: A dependently typed functional programming language and proof assistant
Agda.Compiler.Epic.Smashing
Description
Smash functions which return something that can be inferred (something of a type with only one element)
Synopsis
defnPars :: Integral n => Defn -> nSource
smash'em :: [Fun] -> Compile TCM [Fun]Source
Main function, smash as much as possible
(+++) :: Telescope -> Telescope -> TelescopeSource
inferable :: Set QName -> QName -> [Arg Term] -> Compile TCM (Maybe Expr)Source
Can a datatype be inferred? If so, return the only possible value.
smashable :: Int -> Type -> Compile TCM (Maybe Expr)Source
Find the only possible value for a certain type. If we fail return Nothing
buildLambda :: (Ord n, Num n) => n -> Expr -> ExprSource