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

Safe Haskell | None

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 -> n
- smash'em :: [Fun] -> Compile TCM [Fun]
- (+++) :: Telescope -> Telescope -> Telescope
- inferable :: Set QName -> QName -> [Arg Term] -> Compile TCM (Maybe Expr)
- inferableTerm :: Set QName -> Term -> Compile TCM (Maybe Expr)
- smashable :: Int -> Type -> Compile TCM (Maybe Expr)
- buildLambda :: (Ord n, Num n) => n -> Expr -> Expr

# 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