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

Safe HaskellNone

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 -> ExprSource