diff --git a/ats-format.cabal b/ats-format.cabal
--- a/ats-format.cabal
+++ b/ats-format.cabal
@@ -1,5 +1,5 @@
 name:                ats-format
-version:             0.1.0.6
+version:             0.1.0.7
 synopsis:            A source-code formatter for ATS
 description:         An opinionated source-code formatter for ATS (http://www.ats-lang.org/).
 homepage:            https://hub.darcs.net/vmchale/ats-format#readme
diff --git a/src/Language/ATS/Lexer.x b/src/Language/ATS/Lexer.x
--- a/src/Language/ATS/Lexer.x
+++ b/src/Language/ATS/Lexer.x
@@ -58,7 +58,7 @@
 @string = \" ($printable # [\"] | @escape_str | $esc_char | \n)* \"
 
 -- Identifiers
-@identifier = $alpha ($alpha | $digit | _ | !)*
+@identifier = $alpha ($alpha | $digit | _ | ! | ')*
 
 -- Multi-line comments
 @not_close_paren = (\*+ [^\)] | [^\*] \))
@@ -78,11 +78,11 @@
 @lambda = "=>" | "=<cloref1>" | "=<cloptr1>" | "=>>" | "=<lincloptr1>"
 
 -- FIXME whatever the fuck this is: -<cloptr,fe>
-@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,cloptr1>" | "-<fun0>" | "-<lin,prf>" | "-<>" | "-<prf>" -- FIXME allow spaces after comma?
+@func_type = "-<fun>" | "-<cloptr1>" | "-<lincloptr1>" | "-<lin,cloptr1>" | "-<fun0>" | "-<lin,prf>" | "-<>" | "-<prf>" | "->" -- FIXME allow spaces after comma?
 
 @at_brace = \@ ($white | @block_comment)* \{
 
-@operator = "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "&&" | "||" | "->" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |
+@operator = "+" | "-" | "*" | "/" | ".." | "!=" | ">=" | "<=" | "==" | "=" | "~" | "&&" | "||" | ":=" | ".<" | ">." | "<" | ">" | ">>" | "?" | "?!" | "#[" -- TODO context so tilde doesn't follow |
 
 @double_parens = "(" @block_comment ")" | "()"
 @double_braces = "{" @block_comment "}" | "{}"
@@ -95,8 +95,8 @@
 tokens :-
 
     $white+                  ;
-    ^ @block_comment         { tok (\p s -> CommentLex p s) }
-    ^ "//".*                 { tok (\p s -> CommentLex p s) }
+    ^ @block_comment { tok (\p s -> CommentLex p s) }
+    ^ "//".*         { tok (\p s -> CommentLex p s) }
     "//".*                   ;
     @block_comment           ;
     "#define".*              { tok (\p s -> MacroBlock p s) }      
@@ -169,8 +169,11 @@
     propdef                  { tok (\p s -> Keyword p KwPropdef) }
     tkindef                  { tok (\p s -> Keyword p KwTKind) }
     "$raise"                 { tok (\p s -> Keyword p KwRaise) }
+    mod                      { tok (\p s -> Keyword p KwMod) }
     "println!"               { tok (\p s -> Identifier p s) }
     "prerrln!"               { tok (\p s -> Identifier p s) }
+    "fix@"                   { tok (\p s -> Keyword p KwFixAt) }
+    "lam@"                   { tok (\p s -> Keyword p KwLambdaAt) }
     @double_parens           { tok (\p s -> DoubleParenTok p) }
     @double_braces           { tok (\p s -> DoubleBracesTok p) }
     @double_brackets         { tok (\p s -> DoubleBracketTok p) }
@@ -263,6 +266,9 @@
              | KwPropdef
              | KwRaise
              | KwTKind
+             | KwMod
+             | KwFixAt
+             | KwLambdaAt
              deriving (Eq, Show, Generic, NFData)
 
 data Token = Identifier AlexPosn String
@@ -352,6 +358,9 @@
     pretty KwSortdef = "sortdef"
     pretty KwPropdef = "propdef"
     pretty KwTKind = "tkind"
+    pretty KwMod = "mod"
+    pretty KwFixAt = "fix@"
+    pretty KwLambdaAt = "lambda@"
 
 instance Pretty Token where
     pretty (Identifier _ s) = string s
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
@@ -106,7 +106,7 @@
     neq { Operator $$ "!=" }
     openTermetric { Operator $$ ".<" }
     closeTermetric { Operator $$ ">." }
-    mutateArrow { Operator $$ "->" }
+    mutateArrow { FuncType $$ "->" }
     mutateEq { Operator $$ ":=" }
     lbracket { Operator $$ "<" }
     rbracket { Operator $$ ">" }
@@ -151,6 +151,9 @@
     lineComment { CommentLex _ $$ }
     lspecial { SpecialBracket $$ }
     atbrace { Operator $$ "@{" }
+    mod { Keyword $$ KwMod }
+    fixAt { Keyword $$ KwFixAt }
+    lamAt { Keyword $$ KwLambdaAt }
 
 %%
 
@@ -184,12 +187,13 @@
      | t0pCo { T0p Plus }
      | vt0pPlain { Vt0p None }
      | vt0pCo { Vt0p Plus }
-     | stringType openParen PreExpression closeParen { DepString $3 }
-     | stringType PreExpression { DepString $2 }
-     | int openParen PreExpression closeParen { DependentInt $3 }
-     | bool openParen PreExpression closeParen { DependentBool $3 }
+     | stringType openParen StaticExpression closeParen { DepString $3 }
+     | stringType StaticExpression { DepString $2 }
+     | int openParen StaticExpression closeParen { DependentInt $3 }
+     | bool openParen StaticExpression closeParen { DependentBool $3 }
      | identifier { Named $1 }
      | exclamation Type { Unconsumed $2 }
+     | Type mutateArrow Type { FunctionType "->" $1 $3 }
      | Type funcArrow Type { FunctionType $2 $1 $3 }
      | refType Type { RefType $2 }
      | Type maybeProof { MaybeVal $1 } 
@@ -311,9 +315,9 @@
      | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] }
      | dollar raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$3] } -- we do this because a $raise can have at most one argument
 
-StaticExpression : Name { NamedVal $1 }
-                 | StaticExpression BinOp StaticExpression { Binary $2 $1 $3 }
-                 | intLit { IntLit $1 }
+StaticExpression : Name { StaticVal $1 }
+                 | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }
+                 | intLit { StaticInt $1 }
                  | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions
 
 -- | Parse an expression that can be called without parentheses
@@ -366,7 +370,7 @@
             
 -- | Parse a universal quantifier on a type
 Universal : lbrace Args rbrace { Universal $2 Nothing Nothing }
-          | lbrace Args vbar StaticExpression rbrace { Universal $2 Nothing (Just $4) }
+          | lbrace Args vbar Expression rbrace { Universal $2 Nothing (Just $4) }
 
 -- | Parse the details of an implementation
 Implementation : FunName doubleParens eq Expression { Implement $2 [] [] $1 [] $4 }
@@ -434,6 +438,7 @@
       | or { LogicalOr }
       | doubleEq { StaticEq }
       | eq { Equal }
+      | mod { Mod }
 
 -- | Optionally parse a function body
 OptExpression : { Nothing }
@@ -457,7 +462,7 @@
 
 -- | Parse a type signature and optional function body
 PreFunction : FunName openParen FullArgs closeParen signature Type OptExpression { (PreF $1 $5 [] [] $3 $6 Nothing $7) }
-            | FunName Universals OptTermetric signature Type OptExpression { PreF $1 $4 [] $2 [] $5 $3 $6 }
+            | FunName Universals OptTermetric signature Type OptExpression { PreF $1 $4 [] $2 [NoArgs] $5 $3 $6 }
             | FunName Universals OptTermetric doubleParens signature Type OptExpression { PreF $1 $5 [] $2 [] $6 $3 $7 }
             | FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $1 $7 [] $2 $5 $8 $3 $9 }
             | Universals FunName Universals OptTermetric openParen FullArgs closeParen signature Type OptExpression { PreF $2 $8 $1 $3 $6 $9 $4 $10 }
@@ -518,6 +523,7 @@
             | val Pattern eq Expression { Val $1 Nothing $2 $4 }
             | var Pattern eq PreExpression { Var Nothing $2 (Just $4) Nothing }
             | var Pattern signature Type { Var (Just $4) $2 Nothing Nothing }
+            | var Pattern eq fixAt identifier openParen Args closeParen signature Type plainArrow Expression { Var Nothing $2 (Just $ FixAt (PreF (Unqualified $5) $9 [] [] $7 $10 Nothing (Just $12))) Nothing }
             | prval Pattern eq PreExpression { PrVal $2 $4 }
             | praxi PreFunction { Func $1 (Praxi $2) }
             | primplmnt Implementation { ProofImpl $2 }
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
@@ -99,6 +99,7 @@
     pretty LessThanEq    = "<="
     pretty GreaterThanEq = ">="
     pretty StaticEq      = "=="
+    pretty Mod           = "mod"
 
 splits :: BinOp -> Bool
 splits Mult       = True
@@ -124,7 +125,6 @@
     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 (SifF e e' e'')               = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
         a (LetF _ e (Just e'))          = "let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in" <$> indent 2 e' <$> "end" -- TODO soft linebreak?
         a (LetF _ e Nothing)            = "let" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) e)) <$> "in end"
         a (BoolLitF True)               = "true"
@@ -145,7 +145,7 @@
         a (CallF name [] [] Nothing []) = pretty name <> "()"
         a (CallF name [] [] Nothing [x])
             | startsParens x = pretty name <> pretty x
-        a (CallF name [] [] (Just e) xs) = pretty name <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs
+        a (CallF name [] [] (Just e) xs) = pretty name <> prettyArgsG ("(" <> pretty e <+> "| ") ")" xs -- FIXME split eagerly on "|"
         a (CallF name [] [] Nothing xs) = pretty name <> prettyArgsG "(" ")" xs
         a (CallF name [] us Nothing []) = pretty name <> prettyArgsU "{" "}" us
         a (CallF name is [] Nothing []) = pretty name <> prettyArgsU "<" ">" is
@@ -175,10 +175,11 @@
         a (WhileF _ e e')              = "while" <> parens e <> e'
         a (ActionsF as)                = "{" <$> indent 2 (pretty ((\(ATS x) -> ATS $ reverse x) as)) <$> "}"
         a UnderscoreLitF{}             = "_"
-        a (AtExprF e e')               = e <> "@" <> parens e'
+        a (AtExprF e e')               = e <> "@" <> e'
         a (BeginF _ e)
             | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")
             | otherwise = e
+        a (FixAtF (PreF n s [] [] as t Nothing (Just e))) = "fix@" <+> pretty n <+> prettyArgs as <+> pretty s <> ":" <+> pretty t <+> "=>" </> pretty e
         a _ = "FIXME"
         prettyCases []           = mempty
         prettyCases [(s, t)]     = "|" <+> pretty s <+> "=>" <+> t
@@ -208,7 +209,16 @@
     pretty (Arg (Second t)) = pretty t
     pretty (Arg (Both s t)) = pretty s <+> colon <+> pretty t
     pretty (PrfArg a a')    = pretty a <+> "|" <+> pretty a'
+    pretty NoArgs           = "FIXME"
 
+instance Pretty StaticExpression where
+    pretty = cata a where
+        a (StaticValF n)            = pretty n
+        a (StaticBinaryF op se se') = se <+> pretty op <+> se'
+        a (StaticIntF i)            = pretty i
+        a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
+        a _                         = "FIXME"
+
 instance Pretty Type where
     pretty = cata a where
         a IntF                = "int"
@@ -362,9 +372,11 @@
 fancyU = foldMap pretty . reverse
 
 instance Pretty PreFunction where
+    pretty (PreF i si [] [] [NoArgs] rt Nothing (Just e)) = pretty i <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e) -- FIXME this is an awful hack
     pretty (PreF i si [] [] as rt Nothing (Just e)) = pretty i <> prettyArgs as <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
     pretty (PreF i si [] [] as rt (Just t) (Just e)) = pretty i </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
     pretty (PreF i si [] us as rt (Just t) (Just e)) = pretty i </> fancyU us </> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
+    pretty (PreF i si [] us [NoArgs] rt Nothing (Just e)) = pretty i </> fancyU us <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
     pretty (PreF i si [] us as rt Nothing (Just e)) = pretty i </> fancyU us </> prettyArgs as <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
     pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgs as <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
     pretty (PreF i si pus [] as rt (Just t) (Just e)) = fancyU pus </> pretty i <+> ".<" <> pretty t <> ">." </> prettyArgs as <+> ":" <> string si </> pretty rt <+> "=" <$> indent 2 (pretty e)
@@ -379,12 +391,15 @@
 instance Pretty DataPropLeaf where
     pretty (DataPropLeaf us e) = "|" <+> foldMap pretty (reverse us) <+> pretty e
 
+typeHelper :: [(String, Type)] -> Doc
+typeHelper rs = group (flatAlt ("=" <$> indent 2 (prettyRecord rs)) ("=" <+> prettyRecord rs))
+
 instance Pretty Declaration where
     pretty (RecordType s [] [] rs)   = "typedef" <+> string s <+> "=" <+> prettyRecord rs
     pretty (RecordType s as [] rs)   = "typedef" <+> string s <> prettyArgs as <+> "=" <+> prettyRecord rs
-    pretty (RecordViewType s [] [] rs) = "vtypedef" <+> string s <+> "=" <+> prettyRecord rs
-    pretty (RecordViewType s as [] rs) = "vtypedef" <+> string s <> prettyArgs as <+> "=" <+> prettyRecord rs
-    pretty (RecordViewType s as us rs) = "vtypedef" <+> string s <> prettyArgs as <+> "=" <+> fancyU us </> prettyRecord rs
+    pretty (RecordViewType s [] [] rs) = "vtypedef" <+> string s <+> "=" </> prettyRecord rs
+    pretty (RecordViewType s as [] rs) = "vtypedef" <+> string s <> prettyArgs as <+> typeHelper rs
+    pretty (RecordViewType s as us rs) = "vtypedef" <+> string s <> prettyArgs as <+> "=" </> fancyU us </> prettyRecord rs
     pretty (SumViewType s [] ls) = "datavtype" <+> string s <+> "=" <$> prettyLeaf ls
     pretty (SumViewType s as ls) = "datavtype" <+> string s <> prettyArgs as <+> "=" <$> prettyLeaf ls
     pretty (SumType s [] ls)     = "datatype" <+> string s <+> "=" <$> prettyLeaf ls
@@ -411,8 +426,8 @@
     pretty (Extern _ d)          = "extern" <$> pretty d
     pretty (Define s)            = string s
     pretty (DataProp _ s as ls)  = "dataprop" <+> string s <> prettyArgs as <+> "=" <$> prettyDL ls
-    pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> string s <+> "=" <+> pretty t
-    pretty (ViewTypeDef _ s as t) = "vtypedef" <+> string s <> prettyArgs as <+> "=" <+> pretty t
+    pretty (ViewTypeDef _ s [] t) = "vtypedef" <+> string s <+> "=" </> pretty t
+    pretty (ViewTypeDef _ s as t) = "vtypedef" <+> string s <> prettyArgs as <+> "=" </> pretty t
     pretty (TypeDef _ s [] t)    = "typedef" <+> string s <+> "=" <+> pretty t
     pretty (TypeDef _ s as t)    = "typedef" <+> string s <> prettyArgs as <+> "=" <+> pretty t
     pretty (AbsProp _ n as)      = "absprop" <+> string n <+> prettyArgs as
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
@@ -34,6 +34,8 @@
     , PreFunction (..)
     , Paired (..)
     , Bifurcated (..)
+    , StaticExpression (..)
+    , StaticExpressionF (..)
     , rewriteATS
     ) where
 
@@ -94,9 +96,9 @@
           | Char
           | Int
           | Nat
-          | DependentInt Expression
-          | DependentBool Expression
-          | DepString Expression
+          | DependentInt StaticExpression
+          | DependentBool StaticExpression
+          | DepString StaticExpression
           | Double
           | Float
           | Tuple AlexPosn [Type]
@@ -152,6 +154,7 @@
 -- | An argument to a function.
 data Arg = Arg (Paired String Type)
          | PrfArg Arg Arg
+         | NoArgs
     deriving (Show, Eq, Generic, NFData)
 
 -- | Wrapper for universal quantifiers (refinement types)
@@ -180,8 +183,16 @@
            | LogicalAnd
            | LogicalOr
            | StaticEq
+           | Mod
            deriving (Show, Eq, Generic, NFData)
 
+data StaticExpression = StaticVal Name
+                      | StaticBinary BinOp StaticExpression StaticExpression
+                      | StaticInt Int
+                      | StaticBool Bool
+                      | Sif { scond :: StaticExpression, wwhenTrue :: StaticExpression, selseExpr :: StaticExpression } -- Static if (for proofs)
+                      deriving (Show, Eq, Generic, NFData)
+
 -- | A (possibly effectful) expression.
 data Expression = Let AlexPosn ATS (Maybe Expression)
                 | VoidLiteral -- The '()' literal representing inaction.
@@ -193,7 +204,6 @@
                      , whenTrue :: Expression -- ^ Expression to be returned when true
                      , elseExpr :: Maybe Expression -- ^ Expression to be returned when false
                      }
-                | Sif { cond :: Expression, whenTrue :: Expression, selseExpr :: Expression } -- Static if (for proofs)
                 | BoolLit Bool
                 | TimeLit String
                 | FloatLit Float
@@ -231,6 +241,7 @@
                 | Begin AlexPosn Expression
                 | BinList { _op :: BinOp, _exprs :: [Expression] }
                 | PrecedeList { _exprs :: [Expression] }
+                | FixAt PreFunction
                 deriving (Show, Eq, Generic, NFData)
 
 -- | An 'implement' declaration
@@ -266,6 +277,7 @@
 
 makeBaseFunctor ''Pattern
 makeBaseFunctor ''Expression
+makeBaseFunctor ''StaticExpression
 makeBaseFunctor ''Type
 
 rewriteATS :: Expression -> Expression