Agda.Compiler.Epic.Smashing

Smash functions which return something that can be inferred (something of a type with only one element)

Documentation

defnPars :: Integral n => Defn -> n

smash'em :: [Fun] -> Compile TCM [Fun]

Main function, smash as much as possible

(+++) :: Telescope -> Telescope -> Telescope

inferable :: Set QName -> QName -> [Arg Term] -> Compile TCM (Maybe Expr)

Can a datatype be inferred? If so, return the only possible value.

inferableTerm :: Set QName -> Term -> Compile TCM (Maybe Expr)

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