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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Epic.Smashing

Description

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

Synopsis

Documentation

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 -> Expr Source #