diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,5 +1,5 @@
 name:                language-ats
-version:             0.1.1.14
+version:             0.1.1.15
 synopsis:            Parser and pretty-printer for ATS.
 description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.
 license:             BSD3
diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs
--- a/src/Language/ATS.hs
+++ b/src/Language/ATS.hs
@@ -2,6 +2,7 @@
 module Language.ATS ( -- * Functions for working with syntax
                       lexATS
                     , parseATS
+                    , parseATS'
                     , printATS
                     , printATSCustom
                     , printATSFast
@@ -27,6 +28,7 @@
                     , Existential (..)
                     , PreFunction (..)
                     , StaticExpression (..)
+                    , StackFunction (..)
                     , Paired (..)
                     , Fixity (..)
                     -- * Lexical types
@@ -47,6 +49,10 @@
 import           Language.ATS.Parser
 import           Language.ATS.PrettyPrint
 import           Language.ATS.Types
+
+-- | Parse a string containing ATS source.
+parseATS' :: String -> Either (ATSError String) ATS
+parseATS' = parseATS . lexATS
 
 getDependencies :: ATS -> [FilePath]
 getDependencies (ATS ds) = catMaybes (g <$> ds)
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -351,7 +351,7 @@
            | Expression colon Type { TypeSignature $1 $3 } -- TODO is a more general expression sensible?
            | openParen Expression vbar Expression closeParen { ProofExpr $1 $2 $4 }
            | list_vt lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "vt" $3 $6 }
-           | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 }
+           | list lbrace Type rbrace openParen ExpressionIn closeParen { ListLiteral $1 "" $3 $6 } -- TODO is this legal??
            | begin Expression extern {% Left $ Expected $3 "end" "extern" }
            | Expression prfTransform underscore {% Left $ Expected $2 "Rest of expression or declaration" ">>" }
 
@@ -378,6 +378,11 @@
 StaticArgs : StaticExpression { [$1] }
            | StaticArgs comma StaticExpression { $3 : $1 }
 
+StaticDecls : StaticDeclaration { [$1] }
+            | StaticDecls StaticDeclaration { $2 : $1 }
+            | StaticDecls FunDecl { $2 ++ $1 }
+            | FunDecl StaticDecls { $1 ++ $2 }
+
 StaticExpression : Name { StaticVal $1 }
                  | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }
                  | intLit { StaticInt $1 }
@@ -388,6 +393,10 @@
                  | Name openParen StaticArgs closeParen { SCall $1 $3 }
                  | identifierSpace openParen StaticArgs closeParen { SCall (Unqualified $ to_string $1) $3 }
                  | StaticExpression semicolon StaticExpression { SPrecede $1 $3 }
+                 | UnOp StaticExpression { SUnary $1 $2 }
+                 | identifierSpace doubleParens { SCall (Unqualified $ to_string $1) [] }
+                 | let StaticDecls in end { SLet $1 $2 Nothing }
+                 | let StaticDecls in StaticExpression end { SLet $1 $2 (Just $4) }
     
 -- | Parse an expression that can be called without parentheses
 PreExpression : identifier lsqbracket PreExpression rsqbracket { Index $2 (Unqualified $ to_string $1) $3 }
@@ -468,11 +477,16 @@
 MaybeImplicit : Implicits { $1 }
               | { [] }
 
--- TODO also allow static expressions!
+ImplExpression : StaticExpression { Left $1 }
+               | Expression { Right $1 }
+
 -- | Parse the details of an implementation
-Implementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 $9 }
-               | Universals FunName MaybeImplicit Universals doubleParens eq Expression { Implement $5 $1 $3 $4 $2 [] $7 }
+Implementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq Expression { Implement $5 $1 $3 $4 $2 $6 (Right $9) }
+               | Universals FunName MaybeImplicit Universals doubleParens eq Expression { Implement $5 $1 $3 $4 $2 [] (Right $7) }
 
+StaticImplementation : Universals FunName MaybeImplicit Universals openParen FullArgs closeParen eq StaticExpression { Implement $5 $1 $3 $4 $2 $6 (Left $9) }
+                     | Universals FunName MaybeImplicit Universals doubleParens eq StaticExpression { Implement $5 $1 $3 $4 $2 [] (Left $7) }
+
 -- | Parse a function name
 FunName : IdentifierOr { Unqualified $1 }
         | identifier dollar identifier { Functorial (to_string $1) (to_string $3) }
@@ -611,15 +625,17 @@
           | AndStadef and stadef boolLit eq identifierSpace { AndD $1 (Stadef (over _head toLower (show $4)) (Unqualified $ to_string $6) []) }
           | AndStadef and stadef boolLit eq identifier { AndD $1 (Stadef (over _head toLower (show $4)) (Unqualified $ to_string $6) []) }
 
+StafunDecl : prfun PreFunction { Func $1 (PrFun $2) }
+           | prfn PreFunction { Func $1 (PrFn $2) }
+
 -- | Function declaration
 FunDecl : fun PreFunction { [ Func $1 (Fun $2) ] }
-        | prfun PreFunction { [ Func $1 (PrFun $2) ] }
-        | prfn PreFunction { [ Func $1 (PrFn $2) ] }
         | fnx PreFunction { [ Func $1 (Fnx $2) ] }
         | castfn PreFunction { [ Func $1 (CastFn $2) ] }
         | fn PreFunction identifier {% Left $ Expected (token_posn $3) "=" (to_string $3) }
         | fn PreFunction { [ Func $1 (Fn $2) ] }
         | FunDecl and PreFunction { Func $2 (And $3) : $1 }
+        | StafunDecl { [$1] }
         | extern FunDecl { over _head (Extern $1) $2 }
         | extern fun PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
         | extern fnx PreFunction eq {% Left $ Expected $1 "Declaration" "Function body" }
@@ -684,6 +700,11 @@
         | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }
         | ValDecl and Pattern eq Expression { Val None Nothing $3 $5 : $1 }
 
+StaticDeclaration : prval Pattern eq Expression { PrVal $2 $4 }
+                  | praxi PreFunction { Func $1 (Praxi $2) }
+                  | primplmnt FunArgs StaticImplementation { ProofImpl $2 $3 }
+                  | StafunDecl { $1 }
+
 -- | Parse a declaration
 Declaration : include string { Include $2 }
             | define { Define $1 }
@@ -705,10 +726,8 @@
             | var Pattern colon Type { Var (Just $4) $2 Nothing Nothing }
             | var Pattern eq fixAt IdentifierOr StackFunction { Var Nothing $2 (Just $ FixAt $5 $6) Nothing }
             | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $5) Nothing }
-            | prval Pattern eq Expression { PrVal $2 $4 }
-            | praxi PreFunction { Func $1 (Praxi $2) }
-            | primplmnt FunArgs Implementation { ProofImpl $2 $3 }
             | implement FunArgs Implementation { Impl $2 $3 }
+            | StaticDeclaration { $1 }
             | overload BinOp with Name { OverloadOp $1 $2 $4 }
             | overload identifierSpace with Name { OverloadIdent $1 (to_string $2) $4 Nothing }
             | overload identifierSpace with identifierSpace of intLit { OverloadIdent $1 (to_string $2) (Unqualified $ to_string $4) (Just $6) }
@@ -744,7 +763,7 @@
     pretty (AlexPn _ line col) = pretty line <> ":" <> pretty col
 
 instance Pretty (ATSError String) where
-    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (string s2) <> ", expected:" <+> squotes (string s1)) <> linebreak
+    pretty (Expected p s1 s2) = red "Error: " <> pretty p <> linebreak <> (indent 2 $ "Unexpected" <+> squotes (text s2) <> ", expected:" <+> squotes (text s1)) <> linebreak
     pretty (Unknown (Special l ")")) = red "Error:" <+> "unmatched ')' at" <+> pretty l <> linebreak 
     pretty (Unknown t) = red "Error:" <+> "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak
 
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -56,7 +56,7 @@
 printATSCustom r i (ATS x) = g mempty
     where g = (displayS . renderSmart r i . pretty) (ATS $ reverse x)
 
--- | Fast pretty-printer without indendation. Useful for generating code.
+-- | Slightly faster pretty-printer without indendation (for code generation).
 printATSFast :: ATS -> String
 printATSFast (ATS x) = g mempty
     where g = (displayS . renderCompact . (<> "\n") . pretty) (ATS $ reverse x)
@@ -131,12 +131,9 @@
     pretty = cata a . rewriteATS where
         a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
         a (IfF e e' Nothing)            = "if" <+> e <+> "then" <$> indent 2 e'
-        a (LetF _ e (Just e'))          = flatAlt
-            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end")
-            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in" <+> e' <$> "end")
-        a (LetF _ e Nothing)            = flatAlt
-            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in end")
-            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> "in end")
+        a (LetF _ e e')          = flatAlt
+            ("let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> endLet e')
+            ("let" <+> pretty ((\(ATS x) -> ATS $ reverse x) e) <$> endLet e')
         a (BoolLitF True)               = "true"
         a (BoolLitF False)              = "false"
         a (TimeLitF s)                  = text s
@@ -247,6 +244,10 @@
 squish Mult = True
 squish _    = False
 
+endLet :: Maybe Doc -> Doc
+endLet Nothing  = "in end"
+endLet (Just d) = "in" <$> indent 2 d <$> "end"
+
 instance Pretty StaticExpression where
     pretty = cata a where
         a (StaticValF n)            = pretty n
@@ -260,6 +261,10 @@
         a (StaticBoolF False)       = "false"
         a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))
         a (SPrecedeF e e')          = e <> ";" <+> e'
+        a (SUnaryF Negate e)        = "~" <> e
+        a (SLetF _ e e')          = flatAlt
+            ("let" <$> indent 2 (pretty ((ATS . reverse) e)) <$> endLet e')
+            ("let" <+> pretty ((ATS . reverse) e) <$> endLet e')
 
 instance Pretty Type where
     pretty = cata a where
@@ -335,12 +340,16 @@
 prettyOr [] = mempty
 prettyOr is = mconcat (fmap (prettyArgsU "<" ">") is)
 
+prettyImplExpr :: Either StaticExpression Expression -> Doc
+prettyImplExpr (Left se) = pretty se
+prettyImplExpr (Right e) = pretty e
+
 instance Pretty Implementation where
-    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (pretty e)
-    pretty (Implement _ [] is [] n ias e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
-    pretty (Implement _ [] is us n ias e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
-    pretty (Implement _ ps is [] n ias e) = foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
-    pretty (Implement _ ps is us n ias e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is [] n ias e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is us n ias e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ ps is [] n ias e) = foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ ps is us n ias e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
 
 isVal :: Declaration -> Bool
 isVal Val{}   = True
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -235,6 +235,8 @@
                       | StaticVoid AlexPosn
                       | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs)
                       | SCall Name [StaticExpression]
+                      | SUnary UnOp StaticExpression
+                      | SLet AlexPosn [Declaration] (Maybe StaticExpression)
                       deriving (Show, Eq, Generic, NFData)
 
 -- | A (possibly effectful) expression.
@@ -306,11 +308,11 @@
                                 , universalsI    :: [Universal] -- ^ Universal quantifiers
                                 , nameI          :: Name -- ^ Name of the template being implemented
                                 , iArgs          :: [Arg] -- ^ Arguments
-                                , iExpression    :: Expression -- ^ Expression holding the function body.
+                                , iExpression    :: Either StaticExpression Expression -- ^ Expression (or static expression) holding the function body.
                                 }
     deriving (Show, Eq, Generic, NFData)
 
--- | A function declaration accounting for all three keywords (???) ATS uses to
+-- | A function declaration accounting for all keywords ATS uses to
 -- define them.
 data Function = Fun PreFunction
               | Fn PreFunction