free-compiler-0.3.0.0: A Haskell to Coq compiler.

Safe HaskellNone
LanguageHaskell2010

FreeC.Backend.Agda.Converter.Size

Synopsis
  • size :: Expr
  • up :: Expr -> Expr

Documentation

size :: Expr Source #

Hidden Size argument.

Size

up :: Expr -> Expr Source #

Applies Agda function for larger size.

e ↦ ↑ e