diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.18
 name: language-ats
-version: 1.2.0.16
+version: 1.3.0.0
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018 Vanessa McHale
@@ -38,12 +38,14 @@
         Language.ATS.Parser
         Language.ATS.PrettyPrint
         Language.ATS.Types
+        Language.ATS.Types.Lens
+        Language.ATS.Rewrite
     default-language: Haskell2010
     other-extensions: OverloadedStrings DeriveGeneric DeriveAnyClass
                       FlexibleContexts FlexibleInstances PatternSynonyms
                       StandaloneDeriving GeneralizedNewtypeDeriving DerivingStrategies
                       DuplicateRecordFields DeriveFunctor TypeFamilies
-    ghc-options: -Wall
+    ghc-options: -Wall -O2
     build-depends:
         base >=4.9 && <5,
         array -any,
@@ -86,7 +88,7 @@
     main-is: Bench.hs
     hs-source-dirs: bench
     default-language: Haskell2010
-    ghc-options: -Wall
+    ghc-options: -Wall -O2
     build-depends:
         base -any,
         language-ats -any,
diff --git a/src/Language/ATS.hs b/src/Language/ATS.hs
--- a/src/Language/ATS.hs
+++ b/src/Language/ATS.hs
@@ -41,6 +41,7 @@
                     , SortArg (..)
                     , Sort (..)
                     , SortArgs
+                    , Args
                     , Fix
                     -- * Parser State
                     , FixityState
@@ -67,7 +68,9 @@
 import           Language.ATS.Lexer
 import           Language.ATS.Parser
 import           Language.ATS.PrettyPrint
+import           Language.ATS.Rewrite
 import           Language.ATS.Types
+import           Language.ATS.Types.Lens
 import           Lens.Micro
 import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
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
@@ -67,7 +67,7 @@
 @slash_comment = \/\* ([^\/\*] | @not_close_slash | \n)* \*\/
 @block_comment = @paren_comment | @slash_comment
 
-@if_block = "#if" (n | "") ("def" | "") ([^\#] | "#then" | "#print" | \n)+ "#endif" .*
+@if_block = "#if" (n | "") ("def" | "") ([^\#] | "#then" | "#else" | "#print" | \n)+ "#endif" .*
 
 -- Basically anything that can go inside implicit arguments, i.e. anything
 -- necessary to construct a type.
@@ -79,7 +79,7 @@
 @inner_signature = ("!wrt" | "!exn" | "!refwrt" | "!exnwrt" | "!exnrefwrt" | "!exnref" | "0" | "1" | "!all" | "!laz" | "lin" | "fun" | "clo" | "cloptr" | "cloref" | "!ntm" | "!ref" | "prf" | "fe" | @block_comment)
 @inner_signature_mult = (@inner_signature (("," | "") @inner_signature)*) | ""
 
-@lambda = "=>" | "=>>" | "=/=>" | "=<" @inner_signature_mult ">"
+@lambda = "=>" | "=>>" | "=/=>" | "=/=>>" | "=<" @inner_signature_mult ">"
 @signature = ":<" @inner_signature_mult ">" | ":"
 @func_type = "->" | "-<" @inner_signature_mult ">"
 
@@ -241,6 +241,7 @@
     <0> "println!"               { tok (\p s -> alex $ Identifier p s) }
     <0> "fix@"                   { tok (\p _ -> alex $ Keyword p KwFixAt) }
     <0> "lam@"                   { tok (\p _ -> alex $ Keyword p KwLambdaAt) }
+    <0> "llam@"                  { tok (\p _ -> alex $ Keyword p KwLinearLambdaAt) }
     <0> "addr"                   { tok (\p _ -> alex $ Keyword p KwAddr) }
     <0> "addr@"                  { tok (\p _ -> alex $ Keyword p KwAddrAt) }
     <0> "view@"                  { tok (\p _ -> alex $ Keyword p KwViewAt) }
@@ -267,6 +268,9 @@
     <0> @box_record              { tok (\p s -> alex $ Special p "'{") }
     <0> $br / @ref_call          { tok (\p s -> alex $ SpecialBracket p) }
     <0> @signature               { tok (\p s -> alex $ SignatureTok p (tail s)) }
+    <0> "<"                      { tok (\p _ -> alex $ Special p "<") }
+    <0> ">"                      { tok (\p _ -> alex $ Special p ">") }
+    <0> "[]"                     { tok (\p _ -> alex $ Special p "[]") }
     <0> @operator                { tok (\p s -> alex $ Operator p s) }
     <0> @builtin                 { tok (\p s -> alex $ SpecialIdentifier p (tail s)) }
     <0> $special                 { tok (\p s -> alex $ Special p s) }
@@ -401,6 +405,7 @@
              | KwMod
              | KwFixAt
              | KwLambdaAt
+             | KwLinearLambdaAt
              | KwAddrAt
              | KwAddr
              | KwSta
@@ -461,7 +466,7 @@
     pretty (KwVtype a) = "vtype" <> pretty a
     pretty KwAnd = "and"
     pretty KwDatatype = "datatype"
-    pretty KwDatavtype = "datavtype" -- FIXME this wrongly squashes dataviewtype
+    pretty KwDatavtype = "datavtype"
     pretty KwFnx = "fnx"
     pretty KwAssume = "assume"
     pretty KwAbsimpl = "absimpl"
@@ -525,6 +530,7 @@
     pretty KwMod = "mod"
     pretty KwFixAt = "fix@"
     pretty KwLambdaAt = "lam@"
+    pretty KwLinearLambdaAt = "llam@"
     pretty KwAddrAt = "addr@"
     pretty KwAddr = "addr"
     pretty KwSta = "sta"
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
@@ -10,7 +10,17 @@
                                , preErr
                                ) where
 
+import Control.Composition
+import Control.DeepSeq (NFData)
+import qualified Data.Map as M
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.State
+import Data.Char (toLower)
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Foldable (toList)
+import GHC.Generics (Generic)
 import Language.ATS.Types
+import Language.ATS.Types.Lens
 import Language.ATS.Lexer ( Token (..)
                           , AlexPosn (..)
                           , Keyword (..)
@@ -20,15 +30,7 @@
                           , get_addendum
                           , get_staload
                           )
-
-import Control.Composition
-import Control.DeepSeq (NFData)
 import Lens.Micro (over, _head)
-import qualified Data.Map as M
-import Control.Monad.Trans.Class
-import Control.Monad.Trans.State
-import Data.Char (toLower)
-import GHC.Generics (Generic)
 import Prelude
 import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
@@ -165,8 +167,8 @@
     closeTermetric { Operator $$ ">." }
     mutateArrow { FuncType $$ "->" }
     mutateEq { Operator $$ ":=" }
-    lbracket { Operator $$ "<" }
-    rbracket { Operator $$ ">" }
+    lbracket { Special $$ "<" }
+    rbracket { Special $$ ">" }
     eq { Operator $$ "=" }
     or { Operator $$ "||" }
     vbar { Special $$ "|" }
@@ -180,8 +182,10 @@
     lincloref1Arrow { Arrow $$ "=<lin,cloref1>" }
     spear { Arrow $$ "=>>" }
     proofArrow { Arrow $$ "=/=>" }
+    proofSpear { Arrow $$ "=/=>>" }
     lsqbracket { Special $$ "[" }
     rsqbracket { Special $$ "]" }
+    doubleSqBrackets { Special $$ "[]" }
     string { StringTok _ $$ }
     charLit { CharTok _ $$ }
     underscore { Special $$ "_" }
@@ -216,6 +220,7 @@
     mod { Keyword $$ KwMod }
     fixAt { Keyword $$ KwFixAt }
     lamAt { Keyword $$ KwLambdaAt }
+    llamAt { Keyword $$ KwLinearLambdaAt }
     infixr { FixityTok $$ "infixr" }
     infixl { FixityTok $$ "infixl" }
     prefix { FixityTok $$ "prefix" }
@@ -235,8 +240,8 @@
     : some(p) p { $2 : $1 }
     | { [] }
 
-sep_by(p,sep) : p { [$1] }
-              | sep_by(p,sep) sep p { $3 : $1 }
+sep_by(p,sep) : p { $1 :| [] }
+              | sep_by(p,sep) sep p { $3 :| (toList $1) }
 
 comma_sep(p)
     : sep_by(p, comma) { $1 }
@@ -261,7 +266,7 @@
 
 ExprType : StaticExpression { ConcreteType $1 }
 
-TypeInExpr : comma_sep(alt(Type,ExprType)) { $1 }
+TypeInExpr : comma_sep(alt(Type,ExprType)) { toList $1 }
 
 -- | Parse a type
 Type : Name parens(TypeInExpr) { Dependent $1 $2 }
@@ -289,8 +294,8 @@
      | atbrace Records rbrace { AnonymousRecord $1 $2 }
      | openParen TypeIn vbar Type closeParen { ProofType $1 $2 $4 }
      | identifierSpace identifier { Dependent (Unqualified $ to_string $1) [Named (Unqualified $ to_string $2)] }
-     | openParen TypeIn closeParen { Tuple $1 $2 }
-     | openParen TypeIn closeParen lineComment { Tuple $1 $2 }
+     | openParen TypeIn closeParen { Tuple $1 (toList $2) }
+     | openParen TypeIn closeParen lineComment { Tuple $1 (toList $2) }
      | boxTuple TypeIn closeParen { BoxTuple $1 $2 }
      | boxTuple TypeIn closeParen lineComment { BoxTuple $1 $2 }
      | openParen Type closeParen { ParenType $1 $2 }
@@ -328,7 +333,7 @@
         | doubleParens { VoidLiteral $1 }
 
 -- | Parse a list of comma-separated patterns
-PatternIn : comma_sep(Pattern) { $1 }
+PatternIn : comma_sep(Pattern) { reverse (toList $1) }
 
 -- | Parse a pattern match
 Pattern : Name { PName $1 [] }
@@ -369,15 +374,16 @@
               | ExpressionIn vbar ExpressionIn { (Just $1, $3) } -- FIXME only passes one proof?
 
 -- | A list of comma-separated expressions
-ExpressionIn : comma_sep(Expression) { $1 }
+ExpressionIn : comma_sep(Expression) { toList $1 }
 
-Tuple : PreExpression comma PreExpression { [$3, $1] }
-      | Tuple comma PreExpression { $3 : $1 }
+Tuple : PreExpression comma PreExpression { $3 :| [$1] }
+      | Tuple comma PreExpression { $3 :| toList $1 }
 
 -- | Parse an arrow in a case statement
 CaseArrow : plainArrow { Plain $1 }
           | spear { Spear $1 }
           | proofArrow { ProofArrow $1 }
+          | proofSpear { ProofSpear $1 }
           | minus {% left $ Expected $1 "Arrow" "-" }
           | eq {% left $ Expected $1 "Arrow" "=" }
           | minus {% left $ Expected $1 "Arrow" "-" }
@@ -395,22 +401,21 @@
 -- | Expression or named call to an expression
 Expression : identifierSpace PreExpression { Call (Unqualified $ to_string $1) [] [] Nothing [$2] }
            | PreExpression { $1 }
-           | openParen PreExpression comma PreExpression vbar PreExpression closeParen { TupleEx $1 [$2, $4, $6] } -- FIXME this is wrong
+           -- | openParen PreExpression comma PreExpression vbar PreExpression closeParen { ProofExpr $1 [$2, $4] $6 }
+           | openParen comma_sep(PreExpression) vbar PreExpression closeParen { ProofExpr $1 $2 $4 }
            | Expression semicolon Expression { Precede $1 $3 }
            | Expression semicolon { $1 }
            | openParen Expression closeParen { $2 }
            | 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 }
            | begin Expression extern {% left $ Expected $3 "end" "extern" }
            | Expression prfTransform underscore {% left $ Expected $2 "Rest of expression or declaration" ">>" }
 
-TypeArgs : lbrace Type rbrace { [$2] }
-         | lbrace TypeIn rbrace { $2 }
-         | TypeArgs lbrace Type rbrace { $3 : $1 }
+TypeArgs : lbrace alt(Type,ExprType) rbrace { [$2] }
+         | lbrace TypeInExpr rbrace { $2 }
+         | TypeArgs lbrace alt(Type,ExprType) rbrace { $3 : $1 }
          | lbrace doubleDot rbrace { [ ImplicitType $2 ] } -- FIXME only valid on function calls
-         | TypeArgs lbrace TypeIn rbrace { $3 ++ $1 }
-         | TypeArgs lbrace StaticExpression rbrace { (ConcreteType $3) : $1 }
+         | TypeArgs lbrace TypeInExpr rbrace { $3 ++ $1 }
 
 Call : Name doubleParens { Call $1 [] [] Nothing [] }
      | Name openParen ExpressionPrf closeParen { Call $1 [] [] (fst $3) (snd $3) }
@@ -422,10 +427,11 @@
      | Name Implicits openParen ExpressionPrf closeParen { Call $1 $2 [] (fst $4) (snd $4) }
      | Name Implicits { Call $1 $2 [] Nothing [] }
      | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument
+     | Name Implicits openParen ExpressionPrf fun {% left $ Expected $5 ")" "fun" }
      | Name openParen ExpressionPrf end {% left $ Expected $4 ")" "end"}
      | Name openParen ExpressionPrf else {% left $ Expected $4 ")" "else"}
 
-StaticArgs : comma_sep(StaticExpression) { $1 }
+StaticArgs : comma_sep(StaticExpression) { reverse (toList $1) }
 
 StaticDecls : StaticDeclaration { [$1] }
             | StaticDecls StaticDeclaration { $2 : $1 }
@@ -436,7 +442,7 @@
                  | StaticExpression BinOp StaticExpression { StaticBinary $2 $1 $3 }
                  | intLit { StaticInt $1 }
                  | doubleParens { StaticVoid $1 }
-                 | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 } -- TODO separate type for static expressions
+                 | sif StaticExpression then StaticExpression else StaticExpression { Sif $2 $4 $6 }
                  | identifierSpace { StaticVal (Unqualified $ to_string $1) }
                  | identifierSpace StaticExpression { SCall (Unqualified $ to_string $1) [$2] }
                  | Name openParen StaticArgs closeParen { SCall $1 $3 }
@@ -459,7 +465,7 @@
               | ifcase IfCase { IfCase $1 $2 }
               | openParen Expression closeParen { ParenExpr $1 $2 }
               | PreExpression BinOp PreExpression { Binary $2 $1 $3 }
-              | UnOp PreExpression { Unary $1 $2 } -- FIXME throw error when we try to negate a string literal/time
+              | UnOp PreExpression { Unary $1 $2 }
               | PreExpression dot Name { Access $2 $1 $3 }
               | PreExpression dot intLit { Access $2 $1 (Unqualified $ show $3) }
               | PreExpression dot identifierSpace { Access $2 $1 (Unqualified $ to_string $3) }
@@ -528,7 +534,7 @@
      | IdentifierOr { NamedSort $1 }
      | IdentifierOr plus { NamedSort ($1 <> "+") }
 
-QuantifierArgs : comma_sep(IdentifierOr) { $1 }
+QuantifierArgs : comma_sep(IdentifierOr) { reverse (toList $1) }
                | { [] }
 
 -- FIXME handle [l:addr;n:int]
@@ -548,19 +554,16 @@
           | lbrace QuantifierArgs colon Sort rbrace { Universal $2 (Just $4) [] }
           | lbrace QuantifierArgs colon Sort vbar Predicates rbrace { Universal $2 (Just $4) $6 }
 
-Implicits : lspecial TypeIn rbracket { [$2] }
-          | Implicits lspecial TypeIn rbracket { $3 : $1 }
+Implicits : lspecial TypeIn rbracket { [toList $2] }
+          | Implicits lspecial TypeIn rbracket { toList $3 : $1 }
           | doubleBrackets { [[Named (Unqualified "")]] }
           | Implicits doubleBrackets { [Named (Unqualified "")] : $1 }
-          | lbracket TypeIn rbracket { [$2] }
-          | Implicits lspecial TypeIn rbracket { $3 : $1 }
+          | lbracket TypeIn rbracket { [toList $2] }
+          | Implicits lspecial TypeIn rbracket { toList $3 : $1 }
           
 MaybeImplicit : Implicits { $1 }
               | { [] }
 
-ImplExpression : StaticExpression { Left $1 }
-               | Expression { Right $1 }
-
 comment_after(p) : p { $1 }
                  | p Comment { $1 }
                  | p lineComment { $1 }
@@ -599,12 +602,12 @@
 Records : IdentifierOr eq Type { [($1, $3)] }
         | Records comma IdentifierOr eq Type { ($3, $5) : $1 }
 
-IdentifiersIn : comma_sep(IdentifierOr) { $1 }
+IdentifiersIn : comma_sep(IdentifierOr) { toList $1 }
 
 OfType : { Nothing }
        | of Type { Just $2 }
 
-StaticExpressionsIn : comma_sep(StaticExpression) { $1 }
+StaticExpressionsIn : comma_sep(StaticExpression) { toList $1 }
 
 -- | Parse a constructor for a sum type
 SumLeaf : vbar Universals identifier { Leaf $2 (to_string $3) [] Nothing }
@@ -616,13 +619,15 @@
        | Leaves SumLeaf { $2 : $1 }
        | Universals identifierSpace of Type { [Leaf $1 (to_string $2) [] (Just $4)] }
        | Universals identifier { [Leaf $1 (to_string $2) [] Nothing] }
-       | Universals identifier openParen StaticExpressionsIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] } -- FIXME should take any static expression.
+       | Universals identifier openParen StaticExpressionsIn closeParen OfType { [Leaf $1 (to_string $2) $4 $6] }
        | dollar {% left $ Expected $1 "|" "$" }
 
-Universals : { [] }
-           | doubleBraces { [] }
-           | Universals Universal { $2 : $1 }
+PreUniversals : { [] }
+              | doubleBraces { [] }
+              | PreUniversals Universal { $2 : $1 }
 
+Universals : PreUniversals { reverse $1 }
+
 -- | Optionally parse a termetric
 OptTermetric : { Nothing }
              | Termetric { Just (snd $1) }
@@ -664,6 +669,9 @@
               | eq lineComment fun {% left $ Expected $3 "Expression" "=" }
               | lbrace {% left $ Expected $1 "Expression" "{" }
 
+OptStaticExpression : { Nothing }
+                    | eq StaticExpression { Just $2 }
+
 -- | Parse a constructor for a 'dataprop'
 DataPropLeaf : vbar Universals Expression { DataPropLeaf $2 $3 Nothing }
              | Universals Expression { DataPropLeaf $1 $2 Nothing }
@@ -693,13 +701,13 @@
         | { Nothing }
 
 -- | Parse a type signature and optional function body
-PreFunction : FunName openParen Args closeParen OptType OptExpression { (PreF $1 (fmap fst $5) [] [] $3 (fmap snd $5) Nothing $6) }
-            | FunName Universals OptTermetric OptType OptExpression { PreF $1 (fmap fst $4) [] $2 [NoArgs] (fmap snd $4) $3 $5 }
-            | FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $1 (fmap fst $5) [] $2 [] (fmap snd $5) $3 $6 }
-            | FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 $5 (fmap snd $7) $3 $8 }
-            | Universals FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 $6 (fmap snd $8) $4 $9 }
-            | Universals FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $2 (fmap fst $6) $1 $3 [] (fmap snd $6) $4 $7 }
-            | Universals FunName Universals OptTermetric OptType OptExpression { PreF $2 (fmap fst $5) $1 $3 [] (fmap snd $5) $4 $6 }
+PreFunction : FunName openParen Args closeParen OptType OptExpression { (PreF $1 (fmap fst $5) [] [] (Just $3) (fmap snd $5) Nothing $6) }
+            | FunName Universals OptTermetric OptType OptExpression { PreF $1 (fmap fst $4) [] $2 Nothing (fmap snd $4) $3 $5 }
+            | FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $1 (fmap fst $5) [] $2 (Just []) (fmap snd $5) $3 $6 }
+            | FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $1 (fmap fst $7) [] $2 (Just $5) (fmap snd $7) $3 $8 }
+            | Universals FunName Universals OptTermetric openParen Args closeParen OptType OptExpression { PreF $2 (fmap fst $8) $1 $3 (Just $6) (fmap snd $8) $4 $9 }
+            | Universals FunName Universals OptTermetric doubleParens OptType OptExpression { PreF $2 (fmap fst $6) $1 $3 (Just []) (fmap snd $6) $4 $7 }
+            | Universals FunName Universals OptTermetric OptType OptExpression { PreF $2 (fmap fst $5) $1 $3 Nothing (fmap snd $5) $4 $6 }
             | prval {% left $ Expected $1 "Function signature" "prval" }
             | var {% left $ Expected $1 "Function signature" "var" }
             | val {% left $ Expected (token_posn $1) "Function signature" "val" }
@@ -755,9 +763,9 @@
 MaybeType : eq Type { Just $2 }
           | { Nothing }
 
-FunArgs : { [NoArgs] }
-        | openParen Args closeParen { $2 }
-        | doubleParens { [] }
+FunArgs : { Nothing }
+        | openParen Args closeParen { Just $2 }
+        | doubleParens { Just [] }
 
 SortArg : IdentifierOr colon Sort { [ SortArg $1 $3 ] }
         | SortArg comma IdentifierOr colon Sort { SortArg $3 $5 : $1 }
@@ -772,7 +780,6 @@
          | { Nothing }
 
 SumDecl : datatype IdentifierOr SortArgs eq Leaves { SumType $2 $3 $5 }
-        | datatype IdentifierOr SortArgs eq lineComment Leaves { SumType $2 $3 $6 }
         | datatype lineComment IdentifierOr SortArgs eq Leaves { SumType $3 $4 $6 }
         | datatype lineComment IdentifierOr SortArgs eq lineComment Leaves { SumType $3 $4 $7 }
         | datavtype IdentifierOr SortArgs eq Leaves { SumViewType $2 $3 $5 }
@@ -911,7 +918,7 @@
             | var Pattern eq lamAt StackFunction { Var Nothing $2 (Just $ LambdaAt $4 $5) Nothing }
             | implement FunArgs Implementation { Impl $2 $3 }
             | StaticDeclaration { $1 }
-            | overload lsqbracket rsqbracket with IdentifierOr { OverloadIdent $1 "[]" (Unqualified $5) Nothing }
+            | overload doubleSqBrackets with IdentifierOr { OverloadIdent $1 "[]" (Unqualified $4) Nothing }
             | overload BinOp with Name { OverloadOp $1 $2 $4 Nothing }
             | overload BinOp with customOperator { OverloadOp $1 $2 (Unqualified $ to_string $4) Nothing }
             | overload BinOp with identifierSpace of intLit { OverloadOp $1 $2 (Unqualified $ to_string $4) (Just $6) }
@@ -920,7 +927,7 @@
             | overload identifierSpace with identifierSpace of intLit { OverloadIdent $1 (to_string $2) (Unqualified $ to_string $4) (Just $6) }
             | overload tilde with identifier { OverloadIdent $1 "~" (Unqualified $ to_string $4) Nothing } -- FIXME figure out a general solution.
             | overload tilde with identifierSpace of intLit { OverloadIdent $1 "~" (Unqualified $ to_string $4) (Just $6) }
-            | overload lsqbracket rsqbracket with identifierSpace of intLit { OverloadIdent $1 "[]" (Unqualified $ to_string $5) (Just $7) }
+            | overload doubleSqBrackets with identifierSpace of intLit { OverloadIdent $1 "[]" (Unqualified $ to_string $4) (Just $6) }
             | overload dot identifierSpace with Name { OverloadIdent $1 ('.' : (to_string $3)) $5 Nothing }
             | assume identifierSpace SortArgs eq Type { Assume (Unqualified (to_string $2)) $3 $5 }
             | assume Name SortArgs eq Type { Assume $2 $3 $5 }
@@ -929,8 +936,8 @@
             | tkindef IdentifierOr eq string { TKind $1 (Unqualified $2) $4 }
             | TypeDecl { $1 }
             | symintr Names { SymIntr $1 $2 }
-            | stacst IdentifierOr colon Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }
-            | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }
+            | stacst IdentifierOr colon Type OptStaticExpression { Stacst $1 (Unqualified $2) $4 $5 }
+            | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 (Just $4) $7 }
             | exception identifierSpace of doubleParens { Exception (to_string $2) (Tuple $4 mempty) }
             | exception identifierSpace of openParen Type closeParen { Exception (to_string $2) (Tuple $4 [$5]) }
             | Fixity Operators {% addSt $1 $2 }
@@ -958,6 +965,7 @@
               | OneOf AlexPosn [String] String
               | Unknown Token
               | LexError String
+              | Exhausted
               deriving (Eq, Show, Generic, NFData)
 
 unmatched :: AlexPosn -> String -> Doc
@@ -980,11 +988,13 @@
 preErr (Unknown (Special l ">")) = unmatched l ">"
 preErr (Unknown t) = "unexpected token" <+> squotes (pretty t) <+> "at" <+> pretty (token_posn t) <> linebreak
 preErr (LexError s) = dullred "lexing:" <+> text s <> linebreak
+preErr Exhausted = "unexpectedly out of input"
 
 left :: ATSError -> ParseSt b
 left = lift . Left
 
 parseError :: [Token] -> ParseSt a
-parseError = left . Unknown . head 
+parseError [] = left Exhausted 
+parseError x = left . Unknown . head $ x
 
 }
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
@@ -5,7 +5,6 @@
 {-# LANGUAGE FlexibleContexts   #-}
 {-# LANGUAGE FlexibleInstances  #-}
 {-# LANGUAGE OverloadedStrings  #-}
-{-# LANGUAGE PatternSynonyms    #-}
 {-# LANGUAGE StandaloneDeriving #-}
 
 module Language.ATS.PrettyPrint ( printATS
@@ -15,7 +14,11 @@
 
 import           Control.Composition          hiding ((&))
 import           Data.Bool                    (bool)
+import           Data.Foldable                (toList)
 import           Data.Functor.Foldable        (cata)
+import           Data.List                    (isPrefixOf)
+import           Data.List.NonEmpty           (NonEmpty (..))
+import qualified Data.List.NonEmpty           as NE
 import           Language.ATS.Types
 import           Lens.Micro
 import           Prelude                      hiding ((<$>))
@@ -23,9 +26,6 @@
 
 infixr 5 $$
 
-pattern NoA :: [Arg a]
-pattern NoA = [NoArgs]
-
 -- | Pretty-print with sensible defaults.
 printATS :: Eq a => ATS a -> String
 printATS = (<> "\n") . printATSCustom 0.6 120
@@ -53,6 +53,7 @@
     pretty Plain{}      = "=>"
     pretty Spear{}      = "=>>"
     pretty ProofArrow{} = "=/=>"
+    pretty ProofSpear{} = "=/=>>"
     pretty (Full _ v)   = "=<" <> text v <> ">"
 
 instance Pretty (BinOp a) where
@@ -100,7 +101,6 @@
 prettyLarge _ []      = mempty
 prettyLarge op (e:es) = e <$> vsep (fmap (op <+>) es)
 
--- FIXME we really need a monadic pretty printer lol.
 lengthAlt :: Doc -> Doc -> Doc
 lengthAlt d1 d2
     | length (showFast d2) >= 30 = d1 <$> indent 4 d2
@@ -115,6 +115,10 @@
     pretty Deref           = "!"
     pretty (SpecialOp _ s) = text s
 
+prettyProofExpr :: NonEmpty Doc -> Doc
+prettyProofExpr (e:|[]) = e
+prettyProofExpr es      = mconcat (punctuate ", " (toList es))
+
 instance Eq a => Pretty (Expression a) where
     pretty = cata a where
         a (IfF e e' (Just e''))         = "if" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
@@ -137,20 +141,20 @@
             | splits op = e </> pretty op <+> e'
             | otherwise = e <+> pretty op <+> e'
         a (IndexF _ n e)                = pretty n <> brackets e
-        a (NamedValF nam)              = pretty nam
-        a (CallF nam [] [] Nothing []) = pretty nam <> "()"
-        a (CallF nam [] [] e xs) = pretty nam <> prettyArgsProof e xs
-        a (CallF nam [] us Nothing []) = pretty nam <> prettyArgsU "{" "}" us
+        a (NamedValF nam)               = pretty nam
+        a (CallF nam [] [] Nothing [])  = pretty nam <> "()"
+        a (CallF nam [] [] e xs)        = pretty nam <> prettyArgsProof e xs
+        a (CallF nam [] us Nothing [])  = pretty nam <> prettyArgsU "{" "}" us
         a (CallF nam [] us Nothing [x])
             | startsParens x = pretty nam <> prettyArgsU "{" "}" us <> pretty x
-        a (CallF nam [] us e xs) = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
-        a (CallF nam is [] Nothing []) = pretty nam <> prettyImplicits is
+        a (CallF nam [] us e xs)        = pretty nam <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
+        a (CallF nam is [] Nothing [])  = pretty nam <> prettyImplicits is
         a (CallF nam is [] Nothing [x])
             | startsParens x = pretty nam <> prettyImplicits is <> pretty x
-        a (CallF nam is [] e xs) = pretty nam <> prettyImplicits is <> prettyArgsProof e xs
+        a (CallF nam is [] e xs)        = pretty nam <> prettyImplicits is <> prettyArgsProof e xs
         a (CallF nam is us Nothing [x])
             | startsParens x = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> pretty x
-        a (CallF nam is us e xs) = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
+        a (CallF nam is us e xs)        = pretty nam <> prettyImplicits is <> prettyArgsU "{" "}" us <> prettyArgsProof e xs
         a (CaseF _ add' e cs)           = "case" <> pretty add' <+> e <+> "of" <$> indent 2 (prettyCases cs)
         a (IfCaseF _ cs)                = "ifcase" <$> indent 2 (prettyIfCase cs)
         a (VoidLiteralF _)              = "()"
@@ -160,17 +164,17 @@
         a (PrecedeListF es)             = lineAlt (prettyArgsList "; " "(" ")" es) ("(" <> mconcat (punctuate " ; " es) <> ")")
         a (AccessF _ e n)
             | noParens e = e <> "." <> pretty n
-            | otherwise = parens e <> "." <> pretty n
+            | otherwise  = parens e <> "." <> pretty n
         a (CharLitF '\\')              = "'\\\\'"
         a (CharLitF '\n')              = "'\\n'"
         a (CharLitF '\t')              = "'\\t'"
         a (CharLitF '\0')              = "'\\0'"
         a (CharLitF c)                 = "'" <> char c <> "'"
-        a (ProofExprF _ e e')          = "(" <> e <+> "|" <+> e' <> ")"
+        a (ProofExprF _ es e')         = "(" <> prettyProofExpr es <+> "|" <+> e' <> ")"
         a (TypeSignatureF e t)         = e <+> ":" <+> pretty t
         a (WhereExpF e d)              = e <+> "where" <$> braces (" " <> nest 2 (pretty d) <> " ")
-        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (reverse es))
-        a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (reverse es)) <> ")"
+        a (TupleExF _ es)              = parens (mconcat $ punctuate ", " (toList $ NE.reverse es))
+        a (BoxTupleExF _ es)           = "'(" <> mconcat (punctuate ", " (toList $ NE.reverse es)) <> ")"
         a (WhileF _ e e')              = "while" <> parens e <> e'
         a (ForF _ e e')                = "for" <> parens e <> e'
         a (WhileStarF _ us t as e e' Nothing)   = "while*" <> prettyUsNil us <> prettyTermetric (Just t) <> prettyArgs as <+> "=>" <$> indent 4 e <$> indent 4 e'
@@ -181,7 +185,7 @@
         a UnderscoreLitF{}             = "_"
         a (BeginF _ e)
             | not (startsParens e) = linebreak <> indent 2 ("begin" <$> indent 2 e <$> "end")
-            | otherwise = e
+            | otherwise          = e
         a (FixAtF _ n (StackF s as t e))  = "fix@" <+> text n <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
         a (LambdaAtF _ (StackF s as t e)) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" <$> indent 2 (pretty e)
         a (AddrAtF _ e)                   = "addr@" <> e
@@ -190,7 +194,9 @@
         a (CommentExprF c e) = text c <$> e
         a (MacroVarF _ s) = ",(" <> text s <> ")"
         a BinListF{} = undefined -- Shouldn't happen
+
         prettyImplicits = mconcat . fmap (prettyArgsU "<" ">") . reverse
+
         prettyIfCase []              = mempty
         prettyIfCase [(s, l, t)]     = "|" <+> s <+> pretty l <+> t
         prettyIfCase ((s, l, t): xs) = prettyIfCase xs $$ "|" <+> s <+> pretty l <+> t
@@ -204,7 +210,7 @@
 noParens = all (`notElem` ("()" :: String)) . show
 
 patternHelper :: [Doc] -> Doc
-patternHelper ps = mconcat (punctuate ", " (reverse ps))
+patternHelper ps = mconcat (punctuate ", " ps)
 
 instance Eq a => Pretty (Pattern a) where
     pretty = cata a where
@@ -229,7 +235,6 @@
 argHelper _ (Arg (Second t))  = pretty t
 argHelper op (Arg (Both s t)) = pretty s `op` colon `op` pretty t
 argHelper op (PrfArg a a')    = prettyArgs' ", " mempty mempty a </> "|" `op` pretty a'
-argHelper _ NoArgs            = undefined
 
 instance Eq a => Pretty (SortArg a) where
     pretty (SortArg n st) = text n <> ":" <+> pretty st
@@ -257,7 +262,7 @@
         a (StaticIntF i)            = pretty i
         a StaticVoidF{}             = "()"
         a (SifF e e' e'')           = "sif" <+> e <+> "then" <$> indent 2 e' <$> "else" <$> indent 2 e''
-        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . reverse . fmap pretty $ cs))
+        a (SCallF n cs)             = pretty n <> parens (mconcat (punctuate "," . fmap pretty $ cs))
         a (SPrecedeF e e')          = e <> ";" <+> e'
         a (SUnaryF op e)            = pretty op <> e
         a (SLetF _ e e') = flatAlt
@@ -295,11 +300,11 @@
         a (AtExprF _ t t')                 = t <+> "@" <+> pretty t'
         a (AtTypeF _ t)                    = "@" <> t
         a (ProofTypeF _ t t')              = parens (pre' `op` "|" <+> t')
-            where pre' = prettyArgsG mempty mempty t
+            where pre' = prettyArgsG mempty mempty (toList t)
                   op = bool (<+>) (<>) ('\n' `elem` showFast pre')
         a (ConcreteTypeF e)                = pretty e
         a (TupleF _ ts)                    = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
-        a (BoxTupleF _ ts)                 = "'(" <> mconcat (punctuate ", " (fmap pretty (reverse ts))) <> ")"
+        a (BoxTupleF _ ts)                 = "'(" <> mconcat (punctuate ", " (toList $ fmap pretty (NE.reverse ts))) <> ")"
         a (RefTypeF t)                     = "&" <> t
         a (FunctionTypeF s t t')           = t <+> string s <+> t'
         a (ViewLiteralF c)                 = "view" <> pretty c
@@ -321,15 +326,15 @@
     pretty (Existential [] b (Just st) (Just e')) = withHashtag b <> pretty st <> pretty e' <> rbracket
     pretty (Existential [] b Nothing (Just e')) = withHashtag b <> pretty e' <> rbracket
     pretty (Existential [e] b (Just st) Nothing) = withHashtag b <> text e <> ":" <> pretty st <> rbracket
-    pretty (Existential bs b st Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <+> rbracket
-    pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan st <> "|" <+> pretty e <+> rbracket
+    pretty (Existential bs b st Nothing) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <+> rbracket
+    pretty (Existential bs b st (Just e)) = withHashtag b <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan st <> "|" <+> pretty e <+> rbracket
 
 instance Eq a => Pretty (Universal a) where
     pretty (Universal [x] Nothing []) = lbrace <> text x <> rbrace
     pretty (Universal [x] (Just st) []) = lbrace <> text x <> ":" <> pretty st <> rbrace
-    pretty (Universal bs Nothing []) = lbrace <> mconcat (punctuate "," (fmap pretty (reverse bs))) <> rbrace
-    pretty (Universal bs (Just ty) []) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <+> ":" <+> pretty ty <+> rbrace
-    pretty (Universal bs ty es) = lbrace <+> mconcat (punctuate ", " (fmap pretty (reverse bs))) <> gan ty <> "|" <+> mconcat (punctuate "; " (fmap pretty es)) <+> rbrace
+    pretty (Universal bs Nothing []) = lbrace <> mconcat (punctuate "," (fmap pretty bs)) <> rbrace
+    pretty (Universal bs (Just ty) []) = lbrace <+> mconcat (punctuate ", " (fmap pretty bs)) <+> ":" <+> pretty ty <+> rbrace
+    pretty (Universal bs ty es) = lbrace <+> mconcat (punctuate ", " (fmap pretty bs)) <> gan ty <> "|" <+> mconcat (punctuate "; " (fmap pretty es)) <+> rbrace
 
 instance Eq a => Pretty (ATS a) where
     pretty (ATS xs) = concatSame (reverse xs)
@@ -343,12 +348,15 @@
 prettyImplExpr (Right e) = pretty e
 
 instance Eq a => Pretty (Implementation a) where
-    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e)
-    pretty (Implement _ [] is [] n NoA 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 (reverse ps) </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
-    pretty (Implement _ ps is us n ias e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is [] n (Just []) e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is [] n Nothing e)    = pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is [] n (Just ias) e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is us n (Just ias) e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ [] is us n Nothing e) = pretty n <> prettyOr is <+> foldMap pretty us </> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ ps is [] n (Just ias) e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ ps is [] n Nothing e)    = foldMap pretty (reverse ps) </> pretty n <> prettyOr is <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ ps is us n (Just ias) e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (prettyImplExpr e)
+    pretty (Implement _ ps is us n Nothing e) = foldMap pretty (reverse ps) </> pretty n <> prettyOr is </> foldMap pretty us <+> "=" <$> indent 2 (prettyImplExpr e)
 
 isVal :: Declaration a -> Bool
 isVal Val{}   = True
@@ -357,6 +365,9 @@
 isVal PrVar{} = True
 isVal _       = False
 
+notDefine :: String -> Bool
+notDefine = not . ("#define" `isPrefixOf`)
+
 glue :: Declaration a -> Declaration a -> Bool
 glue x y
     | isVal x && isVal y = True
@@ -374,6 +385,8 @@
 glue Comment{} _                   = True
 glue (Func _ Fnx{}) (Func _ And{}) = True
 glue Assume{} Assume{}             = True
+glue (Define s) _ | notDefine s    = True
+glue _ (Define s) | notDefine s    = True
 glue _ _                           = False
 
 concatSame :: Eq a => [Declaration a] -> Doc
@@ -383,7 +396,6 @@
     | glue x x' = pretty x <$> concatSame (x':xs)
     | otherwise = pretty x <> line <$> concatSame (x':xs)
 
--- TODO - soft break
 ($$) :: Doc -> Doc -> Doc
 x $$ y = align (x <$> y)
 
@@ -396,7 +408,7 @@
 prettyRecord :: (Pretty a) => [(String, a)] -> Doc
 prettyRecord es
     | any ((>40) . length . showFast . pretty) es = prettyRecordF True es
-    | otherwise = lineAlt (prettyRecordF True es) (prettyRecordS True es)
+    | otherwise                                   = lineAlt (prettyRecordF True es) (prettyRecordS True es)
 
 prettyRecordS :: (Pretty a) => Bool -> [(String, a)] -> Doc
 prettyRecordS _ []             = mempty
@@ -414,7 +426,7 @@
 
 prettyUsNil :: Eq a => [Universal a] -> Doc
 prettyUsNil [] = space
-prettyUsNil us = space <> foldMap pretty (reverse us) <> space
+prettyUsNil us = space <> foldMap pretty us <> space
 
 prettyOf :: (Pretty a) => Maybe a -> Doc
 prettyOf Nothing  = mempty
@@ -425,9 +437,6 @@
 prettyDL [DataPropLeaf us e e']    = indent 2 ("|" <> prettyUsNil us <> pretty e <> prettyOf e')
 prettyDL (DataPropLeaf us e e':xs) = prettyDL xs $$ indent 2 ("|" <> prettyUsNil us <> pretty e <> prettyOf e')
 
-universalHelper :: Eq a => [Universal a] -> Doc
-universalHelper = mconcat . fmap pretty . reverse
-
 prettyDSL :: Eq a => [DataSortLeaf a] -> Doc
 prettyDSL []                          = mempty
 prettyDSL [DataSortLeaf us sr sr']    = indent 2 ("|" <> prettyUsNil us <> pretty sr <> prettyOf sr')
@@ -443,14 +452,14 @@
 prettyLeaf [Leaf [] s as (Just e)]    = indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)
 prettyLeaf (Leaf [] s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as)
 prettyLeaf (Leaf [] s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> text s <> prettyArgs as <+> "of" <+> pretty e)
-prettyLeaf [Leaf us s [] Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s)
-prettyLeaf [Leaf us s [] (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)
-prettyLeaf (Leaf us s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s)
-prettyLeaf (Leaf us s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <+> "of" <+> pretty e)
-prettyLeaf [Leaf us s as Nothing]     = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)
-prettyLeaf [Leaf us s as (Just e)]    = indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)
-prettyLeaf (Leaf us s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as)
-prettyLeaf (Leaf us s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> universalHelper us <+> text s <> prettyArgs as <+> "of" <+> pretty e)
+prettyLeaf [Leaf us s [] Nothing]     = indent 2 ("|" <+> fancyU us <+> text s)
+prettyLeaf [Leaf us s [] (Just e)]    = indent 2 ("|" <+> fancyU us <+> text s <+> "of" <+> pretty e)
+prettyLeaf (Leaf us s [] Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s)
+prettyLeaf (Leaf us s [] (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s <+> "of" <+> pretty e)
+prettyLeaf [Leaf us s as Nothing]     = indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as)
+prettyLeaf [Leaf us s as (Just e)]    = indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as <+> "of" <+> pretty e)
+prettyLeaf (Leaf us s as Nothing:xs)  = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as)
+prettyLeaf (Leaf us s as (Just e):xs) = prettyLeaf xs $$ indent 2 ("|" <+> fancyU us <+> text s <> prettyArgs as <+> "of" <+> pretty e)
 
 prettyHelper :: Doc -> [Doc] -> [Doc]
 prettyHelper _ [x]    = [x]
@@ -482,17 +491,16 @@
 prettyArgs :: (Pretty a) => [a] -> Doc
 prettyArgs = prettyArgs' ", " "(" ")"
 
-prettyArgsNil :: Eq a => [Arg a] -> Doc
-prettyArgsNil NoA = mempty
-prettyArgsNil as  = prettyArgs' ", " "(" ")" as
+prettyArgsNil :: Eq a => Maybe [Arg a] -> Doc
+prettyArgsNil Nothing   = mempty
+prettyArgsNil (Just as) = prettyArgs' ", " "(" ")" as
 
 fancyU :: Eq a => [Universal a] -> Doc
-fancyU = foldMap pretty . reverse
+fancyU = foldMap pretty
 
 (<#>) :: Doc -> Doc -> Doc
 (<#>) a b = lineAlt (a <$> indent 2 b) (a <+> b)
 
-
 prettySigG :: (Pretty a) => Doc -> Doc -> Maybe String -> Maybe a -> Doc
 prettySigG d d' (Just si) (Just rt) = d `op` ":" <> text si <#> pretty rt <> d'
     where op a b = lineAlt (a <$> indent 2 b) (a <> b)
@@ -515,7 +523,7 @@
     pretty (PreF i si pus [] as rt Nothing (Just e)) = fancyU pus </> pretty i <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
     pretty (PreF i si pus us as rt t (Just e)) = fancyU pus </> pretty i </> fancyU us <> prettyTermetric t <> prettyArgsNil as <> prettySig si rt <> "=" <$> indent 2 (pretty e)
     pretty (PreF i si [] [] as rt Nothing Nothing) = pretty i <> prettyArgsNil as <> prettySigNull si rt
-    pretty (PreF i si [] us NoA rt Nothing Nothing) = pretty i </> fancyU us <> prettySigNull si rt
+    pretty (PreF i si [] us Nothing rt Nothing Nothing) = pretty i </> fancyU us <> prettySigNull si rt
     pretty (PreF i si [] us as rt Nothing Nothing) = pretty i </> fancyU us </> prettyArgsNil as <> prettySigNull si rt
     pretty (PreF i si pus [] as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> prettyArgsNil as <> prettySigNull si rt
     pretty (PreF i si pus us as rt t Nothing) = fancyU pus </> pretty i <> prettyTermetric t </> fancyU us </> prettyArgsNil as <> prettySigNull si rt
@@ -559,7 +567,7 @@
     pretty (DataView _ s as ls)             = "dataview" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls
     pretty (SumType s as ls)                = "datatype" <+> text s <> prettySortArgs as <+> "=" <$> prettyLeaf ls
     pretty (DataSort _ s ls)                = "datasort" <+> text s <+> "=" <$> prettyDSL ls
-    pretty (Impl as i)                      = "implement" <+> prettyArgsNil as <> pretty i -- mconcat (fmap pretty us) <+> pretty i
+    pretty (Impl as i)                      = "implement" <+> prettyArgsNil as <> pretty i
     pretty (ProofImpl as i)                 = "primplmnt" <+> prettyArgsNil as <> pretty i
     pretty (PrVal p (Just e) Nothing)       = "prval" <+> pretty p <+> "=" <+> pretty e
     pretty (PrVal p Nothing (Just t))       = "prval" <+> pretty p <+> ":" <+> pretty t
@@ -587,7 +595,8 @@
     -- We use 'text' here, which means indentation might get fucked up for
     -- C preprocessor macros, but you absolutely deserve it if you indent your
     -- macros.
-    pretty (Define s)                       = text s
+    pretty (Define s) | "#if" `isPrefixOf` s = text ("\n" <> s)
+                      | otherwise            = text s
     pretty (Func _ (Fn pref))               = "fn" </> pretty pref
     pretty (Func _ (Fun pref))              = "fun" </> pretty pref
     pretty (Func _ (CastFn pref))           = "castfn" </> pretty pref
@@ -605,7 +614,8 @@
     pretty (SymIntr _ ns)                   = "symintr" <+> hsep (fmap pretty ns)
     pretty (Stacst _ n t Nothing)           = "stacst" </> pretty n <+> ":" </> pretty t
     pretty (Stacst _ n t (Just e))          = "stacst" </> pretty n <+> ":" </> pretty t <+> "=" </> pretty e
-    pretty (PropDef _ s as t)               = "propdef" </> text s <+> prettyArgsNil as <+> "=" </> pretty t
+    pretty (PropDef _ s as@Just{} t)        = "propdef" </> text s <+> prettyArgsNil as <+> "=" </> pretty t
+    pretty (PropDef _ s Nothing t)          = "propdef" </> text s <+> "=" </> pretty t
     pretty (Local _ (ATS ds) (ATS []))      = "local" <$> indent 2 (pretty (ATS $ reverse ds)) <$> "in end"
     pretty (Local _ d d')                   = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"
     pretty (FixityDecl f ss)                = pretty f <+> hsep (fmap text ss)
diff --git a/src/Language/ATS/Rewrite.hs b/src/Language/ATS/Rewrite.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS/Rewrite.hs
@@ -0,0 +1,103 @@
+module Language.ATS.Rewrite ( rewriteDecl
+                            -- * Fixity
+                            , defaultFixityState
+                            ) where
+
+import           Control.Composition
+import           Data.Function           (on)
+import           Data.Functor.Foldable
+import qualified Data.Map                as M
+import           Data.Maybe              (isJust)
+import           Language.ATS.Types
+import           Language.ATS.Types.Lens
+import           Lens.Micro
+
+exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t
+exprLens st = flip over (rewriteATS st)
+
+exprLenses :: Eq a => FixityState a -> [ASetter b b (Expression a) (Expression a)] -> b -> b
+exprLenses st = thread . fmap (exprLens st)
+
+rewriteDecl :: Eq a => FixityState a -> Declaration a -> Declaration a
+rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d)
+rewriteDecl st x@Val{} = exprLens st valExpression x
+rewriteDecl st x@Var{} = exprLenses st [varExpr1._Just, varExpr2._Just] x
+rewriteDecl st x@Func{} = exprLens st (fun.preF.expression._Just) x
+rewriteDecl st x@Impl{} = exprLens st (impl.iExpression._Right) x
+rewriteDecl st x@PrVal{} = exprLens st (prValExpr._Just) x
+rewriteDecl st x@AndDecl{} = exprLens st andExpr x
+rewriteDecl st x@DataProp{} = exprLenses st (fmap ((propLeaves.each).) [propExpr1, propExpr2._Just]) x
+rewriteDecl _ x@SumViewType{} = g x
+    where g = over (leaves.mapped.constructorUniversals) h
+          h :: Eq a => [Universal a] -> [Universal a]
+          h = ana c where
+            c (y:y':ys)
+                | typeU y == typeU y' && isJust (typeU y) =
+                    Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys
+            c y = project y
+rewriteDecl _ x = x
+
+-- | Fixities for operators in the ATS prelude.
+defaultFixityState :: FixityState a
+defaultFixityState = M.fromList
+    [ ("::", rightFix 40) ]
+
+leftFix :: Int -> Fixity a
+leftFix = LeftFix undefined . Left
+
+rightFix :: Int -> Fixity a
+rightFix = RightFix undefined . Left
+
+infix_ :: Int -> Fixity a
+infix_ = Infix undefined . Left
+
+-- | Default fixities from @fixity.ats@
+getFixity :: FixityState a -> BinOp a -> Fixity a
+getFixity _ Add                   = leftFix 50
+getFixity _ Sub                   = leftFix 50
+getFixity _ Mutate                = infix_ 0
+getFixity _ Mult                  = leftFix 60
+getFixity _ Div                   = leftFix 60
+getFixity _ SpearOp               = rightFix 10
+getFixity _ LogicalAnd            = leftFix 21
+getFixity _ LogicalOr             = leftFix 20
+getFixity _ At                    = rightFix 40
+getFixity _ GreaterThan           = infix_ 40
+getFixity _ GreaterThanEq         = infix_ 40
+getFixity _ LessThanEq            = infix_ 40
+getFixity _ Equal                 = infix_ 30
+getFixity _ NotEq                 = infix_ 30
+getFixity _ StaticEq              = infix_ 30
+getFixity _ Mod                   = leftFix 60
+getFixity _ LessThan              = infix_ 40
+getFixity st (SpecialInfix _ op') =
+    case M.lookup op' st of
+        (Just f) -> f
+        Nothing  -> infix_ 100
+
+-- FIXME this should account for right vs. left associativity.
+compareFixity :: Eq a => FixityState a -> BinOp a -> BinOp a -> Bool
+compareFixity st = (== GT) .* on compare (getFixity st)
+
+-- | Among other things, this rewrites expressions so that operator precedence
+-- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct
+-- expression.
+rewriteATS :: Eq a => FixityState a -> Expression a -> Expression a
+rewriteATS st = cata a where
+    a (LetF loc (ATS ds) e')                         = Let loc (ATS (rewriteDecl st <$> ds)) e'
+    a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]
+    a (CallF n ts ts' me [ParenExpr _ e@Call{}])     = Call n ts ts' me [e]
+    a (PrecedeF e e'@PrecedeList{})                  = PrecedeList (e : _exprs e')
+    a (PrecedeF e e')                                = PrecedeList [e, e']
+    a (CallF n _ _ _ [Unary (SpecialOp loc s) e])    = Binary (SpecialInfix loc s) (NamedVal n) e
+    a (BinaryF op' (Binary op'' e e') e'')
+        | compareFixity st op' op'' = Binary op'' e (Binary op' e' e'')
+    a (BinaryF Add e (BinList Add es))               = BinList Add (e : es)
+    a (BinaryF Add e e')                             = BinList Add [e, e']
+    a (BinaryF Con{} e (BinList Add es))             = BinList (SpecialInfix undefined "::") (e : es)
+    a (BinaryF Con{} e e')                           = BinList (SpecialInfix undefined "::") [e, e']
+    a (ParenExprF _ e@Precede{})                     = e
+    a (ParenExprF _ e@PrecedeList{})                 = e
+    a (WhereExpF e (ATS ds))                         = WhereExp e (ATS (rewriteDecl st <$> ds))
+    a (ActionsF (ATS ds))                            = Actions (ATS (rewriteDecl st <$> ds))
+    a x                                              = embed x
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
@@ -43,34 +43,20 @@
     , SortF (..)
     , SortArg (..)
     , SortArgs
+    , Args
     , DataSortLeaf (..)
-    , FixityState
     , Fix
-    -- * Rewrites
-    , rewriteDecl
-    -- * Helper functions
-    , defaultFixityState
-    -- * Lenses
-    , preF
-    , expression
-    , fun
-    , leaves
-    , constructorUniversals
-    , typeCall
-    , typeCallArgs
-    , comment
+    , FixityState
     ) where
 
-import           Control.Composition
 import           Control.DeepSeq       (NFData)
 import           Data.Function         (on)
 import           Data.Functor.Foldable hiding (Fix (..))
+import           Data.List.NonEmpty    (NonEmpty)
 import qualified Data.Map              as M
-import           Data.Maybe            (isJust)
 import           Data.Semigroup        (Semigroup)
 import           GHC.Generics          (Generic)
 import           Language.ATS.Lexer    (Addendum (..))
-import           Lens.Micro
 
 type Fix = Either Int String
 
@@ -89,57 +75,13 @@
 data Leaf a = Leaf { _constructorUniversals :: [Universal a], name :: String, constructorArgs :: [StaticExpression a], maybeType :: Maybe (Type a) }
     deriving (Show, Eq, Generic, NFData)
 
-constructorUniversals :: Lens' (Leaf a) [Universal a]
-constructorUniversals f s = fmap (\x -> s { _constructorUniversals = x}) (f (_constructorUniversals s))
-
 type SortArgs a = Maybe [SortArg a]
-
-fun :: Traversal' (Declaration a) (Function a)
-fun f (Func x y) = Func x <$> f y
-fun _ x          = pure x
-
-impl :: Traversal' (Declaration a) (Implementation a)
-impl f (Impl x y)      = Impl x <$> f y
-impl f (ProofImpl x y) = ProofImpl x <$> f y
-impl _ x               = pure x
-
-valExpression :: Traversal' (Declaration a) (Expression a)
-valExpression f (Val a v p e) = Val a v p <$> f e
-valExpression _ x             = pure x
-
-prValExpr :: Traversal' (Declaration a) (Maybe (Expression a))
-prValExpr f (PrVal p me t) = (\me' -> PrVal p me' t) <$> f me
-prValExpr _ x              = pure x
-
-varExpr1 :: Traversal' (Declaration a) (Maybe (Expression a))
-varExpr1 f (Var t p e e') = (\e'' -> Var t p e'' e') <$> f e
-varExpr1 _ x              = pure x
-
-varExpr2 :: Traversal' (Declaration a) (Maybe (Expression a))
-varExpr2 f (Var t p e e') = (\e'' -> Var t p e e'') <$> f e'
-varExpr2 _ x              = pure x
-
-andExpr :: Traversal' (Declaration a) (Expression a)
-andExpr f (AndDecl t p e) = AndDecl t p <$> f e
-andExpr _ x               = pure x
-
-propLeaves :: Traversal' (Declaration a) [DataPropLeaf a]
-propLeaves f (DataProp l n as pl) = DataProp l n as <$> f pl
-propLeaves _ x                    = pure x
-
-leaves :: Traversal' (Declaration a) [Leaf a]
-leaves f (SumType t as l)     = SumType t as <$> f l
-leaves f (SumViewType t as l) = SumViewType t as <$> f l
-leaves _ x                    = pure x
-
-comment :: Traversal' (Declaration a) String
-comment f (Comment c) = Comment <$> f c
-comment _ x           = pure x
+type Args a = Maybe [Arg a]
 
 -- | Declarations for functions, values, actions, etc.
 data Declaration a = Func { pos :: a, _fun :: Function a }
-                   | Impl { implArgs :: [Arg a], _impl :: Implementation a } -- TODO do something better for implicit universals
-                   | ProofImpl { implArgs :: [Arg a], _impl :: Implementation a }
+                   | Impl { implArgs :: Args a, _impl :: Implementation a } -- TODO do something better for implicit universals
+                   | ProofImpl { implArgs :: Args a, _impl :: Implementation a }
                    | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a }
                    | StaVal [Universal a] String (Type a)
                    | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (Expression a), prValType :: Maybe (Type a) }
@@ -174,8 +116,8 @@
                    | Assume (Name a) (SortArgs a) (Type a)
                    | TKind a (Name a) String
                    | SymIntr a [Name a]
-                   | Stacst a (Name a) (Type a) (Maybe (Expression a))
-                   | PropDef a String [Arg a] (Type a)
+                   | Stacst a (Name a) (Type a) (Maybe (StaticExpression a))
+                   | PropDef a String (Args a) (Type a)
                    | FixityDecl (Fixity a) [String]
                    | MacDecl a String [String] (Expression a)
                    | DataSort a String [DataSortLeaf a]
@@ -190,26 +132,20 @@
 data DataPropLeaf a = DataPropLeaf { propU :: [Universal a], _propExpr1 :: Expression a, _propExpr2 :: Maybe (Expression a) }
                     deriving (Show, Eq, Generic, NFData)
 
-propExpr1 :: Lens' (DataPropLeaf a) (Expression a)
-propExpr1 f s = fmap (\x -> s { _propExpr1 = x}) (f (_propExpr1 s))
-
-propExpr2 :: Lens' (DataPropLeaf a) (Maybe (Expression a))
-propExpr2 f s = fmap (\x -> s { _propExpr2 = x}) (f (_propExpr2 s))
-
 -- | A type for parsed ATS types
 data Type a = Tuple a [Type a]
-            | BoxTuple a [Type a]
+            | BoxTuple a (NonEmpty (Type a))
             | Named (Name a)
             | Ex (Existential a) (Maybe (Type a))
             | ForA (Universal a) (Type a)
             | Dependent { _typeCall :: Name a, _typeCallArgs :: [Type a] }
             | Unconsumed (Type a) -- @!a@
-            | AsProof (Type a) (Maybe (Type a)) -- @a >> b@
+            | AsProof (Type a) (Maybe (Type a)) -- @a >> b@ If the second field is 'Nothing' this will print as @a >> _@.
             | FromVT (Type a) -- | @a?!@
             | MaybeVal (Type a) -- | @a?@
             | AtExpr a (Type a) (StaticExpression a)
             | AtType a (Type a)
-            | ProofType a [Type a] (Type a) -- Aka (prf | val)
+            | ProofType a (NonEmpty (Type a)) (Type a) -- Aka (prf | val)
             | ConcreteType (StaticExpression a)
             | RefType (Type a)
             | ViewType a (Type a)
@@ -223,7 +159,7 @@
             deriving (Show, Eq, Generic, NFData)
 
 data TypeF a x = TupleF a [x]
-               | BoxTupleF a [x]
+               | BoxTupleF a (NonEmpty x)
                | NamedF (Name a)
                | ExF (Existential a) (Maybe x)
                | ForAF (Universal a) x
@@ -234,7 +170,7 @@
                | MaybeValF x
                | AtExprF a x (StaticExpression a)
                | AtTypeF a x
-               | ProofTypeF a [x] x
+               | ProofTypeF a (NonEmpty x) x
                | ConcreteTypeF (StaticExpression a)
                | RefTypeF x
                | ViewTypeF a x
@@ -274,20 +210,12 @@
     project (ParenType l ty)           = ParenTypeF l ty
     project (WhereType l ty s sas ty') = WhereTypeF l ty s sas ty'
 
-typeCall :: Traversal' (Type a) (Name a)
-typeCall f (Dependent x y) = (\x' -> Dependent x' y) <$> f x
-typeCall _ x               = pure x
-
-typeCallArgs :: Traversal' (Type a) [Type a]
-typeCallArgs f (Dependent x y) = (\y' -> Dependent x y') <$> f y
-typeCallArgs _ x               = pure x
-
 -- | A type for @=>@, @=\<cloref1>@, etc.
 data LambdaType a = Plain a
                   | Spear a -- | @=>>@
                   | ProofArrow a -- | @=/=>@
+                  | ProofSpear a -- | @=/=>>@
                   | Full a String
-                  -- TODO figure out wtf ProofArrow does
                   deriving (Show, Eq, Generic, NFData)
 
 data Name a = Unqualified String
@@ -357,7 +285,6 @@
 -- | An argument to a function.
 data Arg a = Arg (Paired String (Type a))
            | PrfArg [Arg a] (Arg a)
-           | NoArgs
            deriving (Show, Eq, Generic, NFData)
 
 -- | A datatype for sorts.
@@ -393,7 +320,6 @@
     project (TupleSort x s s') = TupleSortF x s s'
     project (ArrowSort x s s') = ArrowSortF x s s'
 
--- FIXME a type for sorts?
 -- | Wrapper for universal quantifiers (refinement types)
 data Universal a = Universal { bound :: [String], typeU :: Maybe (Sort a), prop :: [StaticExpression a] }
     deriving (Show, Eq, Generic, NFData)
@@ -492,7 +418,7 @@
                   | UnderscoreLit a
                   | Lambda a (LambdaType a) (Pattern a) (Expression a)
                   | LinearLambda a (LambdaType a) (Pattern a) (Expression a)
-                  | Index a (Name a) (Expression a)
+                  | Index a (Name a) (Expression a) -- ^ E.g. @array[0]@.
                   | Access a (Expression a) (Name a)
                   | StringLit String
                   | CharLit Char
@@ -510,13 +436,13 @@
                          }
                   | RecordValue a [(String, Expression a)] (Maybe (Type a))
                   | Precede (Expression a) (Expression a)
-                  | ProofExpr a (Expression a) (Expression a)
+                  | ProofExpr a (NonEmpty (Expression a)) (Expression a)
                   | TypeSignature (Expression a) (Type a)
                   | WhereExp (Expression a) (ATS a)
-                  | TupleEx a [Expression a]
-                  | BoxTupleEx a [Expression a]
+                  | TupleEx a (NonEmpty (Expression a))
+                  | BoxTupleEx a (NonEmpty (Expression a))
                   | While a (Expression a) (Expression a)
-                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Maybe [Arg a]) -- ^ A @while@ loop that is guaranteed to terminate.
+                  | WhileStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) (Args a) -- ^ A @while@ loop that is guaranteed to terminate.
                   | For a (Expression a) (Expression a)
                   | ForStar a [Universal a] (StaticExpression a) [Arg a] (Expression a) (Expression a) -- ^ A @for@ loop that is guaranteed to terminate.
                   | Actions (ATS a)
@@ -555,13 +481,13 @@
                      | CaseF a Addendum x [(Pattern a, LambdaType a, x)]
                      | RecordValueF a [(String, x)] (Maybe (Type a))
                      | PrecedeF x x
-                     | ProofExprF a x x
+                     | ProofExprF a (NonEmpty x) x
                      | TypeSignatureF x (Type a)
                      | WhereExpF x (ATS a)
-                     | TupleExF a [x]
-                     | BoxTupleExF a [x]
+                     | TupleExF a (NonEmpty x)
+                     | BoxTupleExF a (NonEmpty x)
                      | WhileF a x x
-                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Maybe [Arg a])
+                     | WhileStarF a [Universal a] (StaticExpression a) [Arg a] x x (Args a)
                      | ForF a x x
                      | ForStarF a [Universal a] (StaticExpression a) [Arg a] x x
                      | ActionsF (ATS a)
@@ -673,14 +599,11 @@
                                   , implicits      :: [[Type a]] -- ^ Implicit arguments
                                   , universalsI    :: [Universal a] -- ^ Universal quantifiers
                                   , nameI          :: Name a -- ^ ('Name' a) of the template being implemented
-                                  , iArgs          :: [Arg a] -- ^ Arguments
+                                  , iArgs          :: Args a -- ^ Arguments
                                   , _iExpression   :: Either (StaticExpression a) (Expression a) -- ^ Expression (or static expression) holding the function body.
                                   }
     deriving (Show, Eq, Generic, NFData)
 
-iExpression :: Lens' (Implementation a) (Either (StaticExpression a) (Expression a))
-iExpression f s = fmap (\x -> s { _iExpression = x}) (f (_iExpression s))
-
 -- | A function declaration accounting for all keywords ATS uses to
 -- define them.
 data Function a = Fun { _preF :: PreFunction a }
@@ -693,9 +616,6 @@
                 | CastFn { _preF :: PreFunction a }
                 deriving (Show, Eq, Generic, NFData)
 
-preF :: Lens' (Function a) (PreFunction a)
-preF f s = fmap (\x -> s { _preF = x}) (f (_preF s))
-
 -- | A type for stack-allocated functions. See
 -- [here](http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c1267.html)
 -- for more.
@@ -710,109 +630,15 @@
                           , sig           :: Maybe String -- ^ e.g. <> or \<!wrt>
                           , preUniversals :: [Universal a] -- ^ Universal quantifiers making a function generic
                           , universals    :: [Universal a] -- ^ (Universal a) quantifiers/refinement type
-                          , args          :: [Arg a] -- ^ Actual function arguments
+                          , args          :: Args a -- ^ Actual function arguments
                           , returnType    :: Maybe (Type a) -- ^ Return type
                           , termetric     :: Maybe (StaticExpression a) -- ^ Optional termination metric
                           , _expression   :: Maybe (Expression a) -- ^ Expression holding the actual function body (not present in static templates)
                           }
                           deriving (Show, Eq, Generic, NFData)
 
--- TODO lens/base functor module?
-expression :: Lens' (PreFunction a) (Maybe (Expression a))
-expression f s = fmap (\x -> s { _expression = x}) (f (_expression s))
-
-exprLens :: Eq a => FixityState a -> ASetter s t (Expression a) (Expression a) -> s -> t
-exprLens st = flip over (rewriteATS st)
-
-exprLenses :: Eq a => FixityState a -> [ASetter b b (Expression a) (Expression a)] -> b -> b
-exprLenses st = thread . fmap (exprLens st)
-
-rewriteDecl :: Eq a => FixityState a -> Declaration a -> Declaration a
-rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d)
-rewriteDecl st x@Val{} = exprLens st valExpression x
-rewriteDecl st x@Var{} = exprLenses st [varExpr1._Just, varExpr2._Just] x
-rewriteDecl st x@Func{} = exprLens st (fun.preF.expression._Just) x
-rewriteDecl st x@Impl{} = exprLens st (impl.iExpression._Right) x
-rewriteDecl st x@PrVal{} = exprLens st (prValExpr._Just) x
-rewriteDecl st x@AndDecl{} = exprLens st andExpr x
-rewriteDecl st x@DataProp{} = exprLenses st (fmap ((propLeaves.each).) [propExpr1, propExpr2._Just]) x
-rewriteDecl _ x@SumViewType{} = g x
-    where g = over (leaves.mapped.constructorUniversals) h
-          h :: Eq a => [Universal a] -> [Universal a]
-          h = ana c where
-            c (y:y':ys)
-                | typeU y == typeU y' && isJust (typeU y) =
-                    Cons (Universal (bound y ++ bound y') (typeU y) (StaticBinary LogicalAnd <$> prop y <*> prop y')) ys
-            c y = project y
-rewriteDecl _ x = x
-
 -- FIXME left vs. right shouldn't be treated the same
 instance (Eq a) => Ord (Fixity a) where
     compare = on compare ifix
 
-leftFix :: Int -> Fixity a
-leftFix = LeftFix undefined . Left
-
-rightFix :: Int -> Fixity a
-rightFix = RightFix undefined . Left
-
-infix_ :: Int -> Fixity a
-infix_ = Infix undefined . Left
-
 type FixityState a = M.Map String (Fixity a)
-
--- | Fixities for operators in the ATS prelude.
-defaultFixityState :: FixityState a
-defaultFixityState = M.fromList
-    [ ("::", rightFix 40) ]
-
--- | Default fixities from @fixity.ats@
-getFixity :: FixityState a -> BinOp a -> Fixity a
-getFixity _ Add                   = leftFix 50
-getFixity _ Sub                   = leftFix 50
-getFixity _ Mutate                = infix_ 0
-getFixity _ Mult                  = leftFix 60
-getFixity _ Div                   = leftFix 60
-getFixity _ SpearOp               = rightFix 10
-getFixity _ LogicalAnd            = leftFix 21
-getFixity _ LogicalOr             = leftFix 20
-getFixity _ At                    = rightFix 40
-getFixity _ GreaterThan           = infix_ 40
-getFixity _ GreaterThanEq         = infix_ 40
-getFixity _ LessThanEq            = infix_ 40
-getFixity _ Equal                 = infix_ 30
-getFixity _ NotEq                 = infix_ 30
-getFixity _ StaticEq              = infix_ 30
-getFixity _ Mod                   = leftFix 60
-getFixity _ LessThan              = infix_ 40
-getFixity st (SpecialInfix _ op') =
-    case M.lookup op' st of
-        (Just f) -> f
-        Nothing  -> infix_ 100
-
--- FIXME this should account for right vs. left associativity.
-compareFixity :: Eq a => FixityState a -> BinOp a -> BinOp a -> Bool
-compareFixity st = (== GT) .* on compare (getFixity st)
-
--- | Among other things, this rewrites expressions so that operator precedence
--- is respected; this ensures @1 + 2 * 3@ will be parsed as the correct
--- expression.
-rewriteATS :: Eq a => FixityState a -> Expression a -> Expression a
-rewriteATS st = cata a where
-    a (LetF loc (ATS ds) e')                         = Let loc (ATS (rewriteDecl st <$> ds)) e'
-    a (CallF n ts ts' me [ParenExpr _ e@NamedVal{}]) = Call n ts ts' me [e]
-    a (CallF n ts ts' me [ParenExpr _ e@Call{}])     = Call n ts ts' me [e]
-    a (PrecedeF e e'@PrecedeList{})                  = PrecedeList (e : _exprs e')
-    a (PrecedeF e e')                                = PrecedeList [e, e']
-    a (CallF n _ _ _ [Unary (SpecialOp loc s) e])    = Binary (SpecialInfix loc s) (NamedVal n) e
-    a (BinaryF op' (Binary op'' e e') e'')
-        | compareFixity st op' op'' = Binary op'' e (Binary op' e' e'')
-    a (BinaryF Add e (BinList Add es))               = BinList Add (e : es)
-    a (BinaryF Add e e')                             = BinList Add [e, e']
-    a (BinaryF Con{} e (BinList Add es))             = BinList (SpecialInfix undefined "::") (e : es)
-    a (BinaryF Con{} e e')                           = BinList (SpecialInfix undefined "::") [e, e']
-    a (ParenExprF _ e@Precede{})                     = e
-    a (ParenExprF _ e@PrecedeList{})                 = e
-    a (WhereExpF e (ATS ds))                         = WhereExp e (ATS (rewriteDecl st <$> ds))
-    a (ActionsF (ATS ds))                            = Actions (ATS (rewriteDecl st <$> ds))
-    a x                                              = embed x
diff --git a/src/Language/ATS/Types/Lens.hs b/src/Language/ATS/Types/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/ATS/Types/Lens.hs
@@ -0,0 +1,93 @@
+module Language.ATS.Types.Lens ( -- * Lenses
+                                 iExpression
+                               , constructorUniversals
+                               , expression
+                               , preF
+                               , propExpr1
+                               , propExpr2
+                               -- * Traversals
+                               , typeCall
+                               , typeCallArgs
+                               , fun
+                               , impl
+                               , valExpression
+                               , prValExpr
+                               , varExpr1
+                               , varExpr2
+                               , andExpr
+                               , propLeaves
+                               , leaves
+                               , comment
+                               ) where
+
+import           Language.ATS.Types
+import           Lens.Micro
+
+constructorUniversals :: Lens' (Leaf a) [Universal a]
+constructorUniversals f s = fmap (\x -> s { _constructorUniversals = x}) (f (_constructorUniversals s))
+
+expression :: Lens' (PreFunction a) (Maybe (Expression a))
+expression f s = fmap (\x -> s { _expression = x}) (f (_expression s))
+
+preF :: Lens' (Function a) (PreFunction a)
+preF f s = fmap (\x -> s { _preF = x}) (f (_preF s))
+
+iExpression :: Lens' (Implementation a) (Either (StaticExpression a) (Expression a))
+iExpression f s = fmap (\x -> s { _iExpression = x}) (f (_iExpression s))
+
+propExpr1 :: Lens' (DataPropLeaf a) (Expression a)
+propExpr1 f s = fmap (\x -> s { _propExpr1 = x}) (f (_propExpr1 s))
+
+propExpr2 :: Lens' (DataPropLeaf a) (Maybe (Expression a))
+propExpr2 f s = fmap (\x -> s { _propExpr2 = x}) (f (_propExpr2 s))
+
+
+typeCall :: Traversal' (Type a) (Name a)
+typeCall f (Dependent x y) = (\x' -> Dependent x' y) <$> f x
+typeCall _ x               = pure x
+
+typeCallArgs :: Traversal' (Type a) [Type a]
+typeCallArgs f (Dependent x y) = (\y' -> Dependent x y') <$> f y
+typeCallArgs _ x               = pure x
+
+fun :: Traversal' (Declaration a) (Function a)
+fun f (Func x y) = Func x <$> f y
+fun _ x          = pure x
+
+impl :: Traversal' (Declaration a) (Implementation a)
+impl f (Impl x y)      = Impl x <$> f y
+impl f (ProofImpl x y) = ProofImpl x <$> f y
+impl _ x               = pure x
+
+valExpression :: Traversal' (Declaration a) (Expression a)
+valExpression f (Val a v p e) = Val a v p <$> f e
+valExpression _ x             = pure x
+
+prValExpr :: Traversal' (Declaration a) (Maybe (Expression a))
+prValExpr f (PrVal p me t) = (\me' -> PrVal p me' t) <$> f me
+prValExpr _ x              = pure x
+
+varExpr1 :: Traversal' (Declaration a) (Maybe (Expression a))
+varExpr1 f (Var t p e e') = (\e'' -> Var t p e'' e') <$> f e
+varExpr1 _ x              = pure x
+
+varExpr2 :: Traversal' (Declaration a) (Maybe (Expression a))
+varExpr2 f (Var t p e e') = (\e'' -> Var t p e e'') <$> f e'
+varExpr2 _ x              = pure x
+
+andExpr :: Traversal' (Declaration a) (Expression a)
+andExpr f (AndDecl t p e) = AndDecl t p <$> f e
+andExpr _ x               = pure x
+
+propLeaves :: Traversal' (Declaration a) [DataPropLeaf a]
+propLeaves f (DataProp l n as pl) = DataProp l n as <$> f pl
+propLeaves _ x                    = pure x
+
+leaves :: Traversal' (Declaration a) [Leaf a]
+leaves f (SumType t as l)     = SumType t as <$> f l
+leaves f (SumViewType t as l) = SumViewType t as <$> f l
+leaves _ x                    = pure x
+
+comment :: Traversal' (Declaration a) String
+comment f (Comment c) = Comment <$> f c
+comment _ x           = pure x
diff --git a/test/data/concurrency.out b/test/data/concurrency.out
--- a/test/data/concurrency.out
+++ b/test/data/concurrency.out
@@ -113,7 +113,7 @@
   deqarray_make_cap(i2sz(cap))
 
 implement {a} queue_free (que) =
-  deqarray_free_nil($UN.castvwtp0{deqarray(a, 1, 0)}(que))
+  deqarray_free_nil($UN.castvwtp0{deqarray(a,1,0)}(que))
 
 implement {a} channel_ref (chan) =
   let