Agda-2.3.0: A dependently typed functional programming language and proof assistant



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



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

Main function, smash as much as possible

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