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.20
+version:             0.1.0.21
 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
@@ -142,9 +142,12 @@
     void                     { tok (\p s -> Keyword p KwVoid) }
     nat                      { tok (\p s -> Keyword p KwNat) }
     implement                { tok (\p s -> Keyword p KwImplement) }
+    implmnt                  { tok (\p s -> Keyword p KwImplement) }
     primplmnt                { tok (\p s -> Keyword p KwProofImplement) }
-    primplement              { tok (\p s -> Keyword p KwProofImplement) } -- TODO does this squash too much?
+    primplement              { tok (\p s -> Keyword p KwProofImplement) }
     abst"@"ype               { tok (\p s -> Keyword p (KwAbst0p None)) }
+    abst"@ype+"              { tok (\p s -> Keyword p (KwAbst0p Plus)) }
+    abst"@type-"             { tok (\p s -> Keyword p (KwAbst0p Minus)) }
     abs@view"t@ype"          { tok (\p s -> Keyword p (KwAbsvt0p None)) }
     t"@"ype"+"               { tok (\p s -> Keyword p (KwT0p Plus)) }
     t"@"ype"-"               { tok (\p s -> Keyword p (KwT0p Minus)) }
@@ -176,6 +179,7 @@
     sortdef                  { tok (\p s -> Keyword p KwSortdef) }
     propdef                  { tok (\p s -> Keyword p KwPropdef) }
     tkindef                  { tok (\p s -> Keyword p KwTKind) }
+    typekindef               { 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) }
@@ -188,6 +192,8 @@
     sta                      { tok (\p s -> Keyword p KwSta) }
     symintr                  { tok (\p s -> Keyword p KwSymintr) }
     absview                  { tok (\p s -> Keyword p KwAbsview) }
+    "$list"                  { tok (\p s -> Keyword p (KwListLit "")) }
+    "$list_vt"               { tok (\p s -> Keyword p (KwListLit "_vt")) }
     "fold@"                  { tok (\p s -> Identifier p s) }
     "free@"                  { tok (\p s -> Identifier p s) }
     @double_parens           { tok (\p s -> DoubleParenTok p) }
@@ -299,6 +305,7 @@
              | KwInfixr
              | KwInfixl
              | KwStacst
+             | KwListLit String
              deriving (Eq, Show, Generic, NFData)
 
 data Token = Identifier AlexPosn String
@@ -405,6 +412,7 @@
     pretty KwInfix = "infix"
     pretty KwInfixr = "infixr"
     pretty KwInfixl = "infixl"
+    pretty (KwListLit s) = "list" <> string s
 
 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
@@ -100,6 +100,9 @@
     viewAt { Keyword $$ KwViewAt }
     symintr { Keyword $$ KwSymintr }
     stacst { Keyword $$ KwStacst }
+    propdef { Keyword $$ KwPropdef }
+    list { Keyword $$ (KwListLit "") }
+    list_vt { Keyword $$ (KwListLit "_vt") }
     boolLit { BoolTok _ $$ }
     timeLit { TimeTok _ $$ }
     intLit { IntTok _ $$ }
@@ -109,7 +112,6 @@
     extfcall { Identifier $$ "extfcall" }
     ldelay { Identifier $$ "ldelay" }
     listVT { Identifier $$ "list_vt" }
-    -- TODO token? raise { Identifier $$ "raise" }
     identifier { Identifier _ $$ }
     identifierSpace { IdentifierSpace _ $$ }
     closeParen { Special $$ ")" }
@@ -322,6 +324,8 @@
            | openParen Expression closeParen { $2 }
            | Expression signature Type { TypeSignature $1 $3 }
            | 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 }
 
 TypeArgs : lbrace Type rbrace { [$2] }
          | lbrace TypeIn rbrace { $2 }
@@ -339,7 +343,7 @@
      | Name TypeArgs { Call $1 [] $2 Nothing [] }
      | Name lspecial TypeIn rbracket openParen ExpressionPrf closeParen { Call $1 $3 [] (fst $6) (snd $6) }
      | Name lspecial TypeIn rbracket { Call $1 $3 [] Nothing [] }
-     | dollar raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$3] } -- $raise can have at most one argument
+     | raise PreExpression { Call (SpecialName $1 "raise") [] [] Nothing [$2] } -- $raise can have at most one argument
 
 StaticArgs : StaticExpression { [$1] }
            | StaticArgs comma StaticExpression { $3 : $1 }
@@ -617,6 +621,7 @@
             | TypeDecl { $1 }
             | symintr Name { SymIntr $1 $2 }
             | stacst IdentifierOr signature Type OptExpression { Stacst $1 (Unqualified $2) $4 $5 }
+            | propdef IdentifierOr openParen Args closeParen eq Type { PropDef $1 $2 $4 $7 }
             | lambda {% Left $ Expected $1 "Declaration" "lam" }
             | llambda {% Left $ Expected $1 "Declaration" "llam" }
             | minus {% Left $ Expected $1 "Declaration" "-" }
@@ -624,6 +629,7 @@
             | fromVT {% Left $ Expected $1 "Declaration" "?!" }
             | prfTransform {% Left $ Expected $1 "Declaration" ">>" }
             | maybeProof {% Left $ Expected $1 "Declaration" "?" }
+            | end {% Left $ Expected $1 "Declaration" "end" }
 
 {
 
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
@@ -135,7 +135,7 @@
         a (LambdaF _ lt p e)            = "lam" <+> pretty p <+> pretty lt <+> e
         a (LinearLambdaF _ lt p e)      = "llam" <+> pretty p <+> pretty lt <+> e
         a (FloatLitF f)                 = pretty f
-        a (StringLitF s)                = string s
+        a (StringLitF s)                = string s -- FIXME escape indentation in multi-line strings.
         a (ParenExprF _ e)              = parens e
         a (BinListF op@Add es)          = prettyBinary (pretty op) es
         a (BinaryF op e e')
@@ -183,6 +183,7 @@
         a (LambdaAtF (PreF Unnamed{} s [] [] as t Nothing (Just e))) = "lam@" <+> prettyArgs as <+> ":" <> pretty s <+> pretty t <+> "=>" </> pretty e
         a (AddrAtF _ e)                = "addr@" <> e
         a (ViewAtF _ e)                = "view@" <> e
+        a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es
         a _ = "FIXME"
         prettyCases []              = mempty
         prettyCases [(s, l, t)]     = "|" <+> pretty s <+> pretty l <+> t
@@ -480,4 +481,5 @@
     pretty (SymIntr _ n)                = "symintr" <+> pretty n
     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" </> string s <+> prettyArgs as <+> "=" </> pretty t
     pretty _                            = "FIXME"
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
@@ -101,6 +101,7 @@
                  | TKind AlexPosn Name String
                  | SymIntr AlexPosn Name
                  | Stacst AlexPosn Name Type (Maybe Expression)
+                 | PropDef AlexPosn String [Arg] Type
                  deriving (Show, Eq, Generic, NFData)
 
 data DataPropLeaf = DataPropLeaf [Universal] Expression (Maybe Expression)
@@ -224,6 +225,7 @@
                 -- function call: <a>, then {n}
                 | Call Name [Type] [Type] (Maybe Expression) [Expression]
                 | NamedVal Name
+                | ListLiteral AlexPosn String Type [Expression]
                 | If { cond     :: Expression -- ^ Expression evaluating to a boolean value
                      , whenTrue :: Expression -- ^ Expression to be returned when true
                      , elseExpr :: Maybe Expression -- ^ Expression to be returned when false
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -7,6 +7,7 @@
   - htoml-megaparsec-1.0.1.12
   - composition-prelude-0.1.1.4
   - dirstream-1.0.3
+  - hspec-dirstream-0.1.0.1
 flags:
   ats-format:
     development: false