diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,24 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.6.5 — 2023-10-01
+
+This version contains mostly intrastructure improvements:
+
+- Typecheck using `rzk.yaml` if it exists (see [#119](https://github.com/rzk-lang/rzk/pull/119))
+- Update Rzk Playground and Nix Flake (see [#84](https://github.com/rzk-lang/rzk/pull/84))
+  - Rzk Playground now uses CodeMirror 6 and NextJS
+  - `miso` dependency is dropped
+  - GHCJS 9.6 is now used
+  - Support `snippet={code}` or `code={code}` param (see [#118](https://github.com/rzk-lang/rzk/pull/118))
+    - Support for `snippet_url={URL}` is temporarily dropped
+- Update to GHC 9.6, latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116))
+- Add logging for Rzk Language Server (see [#114](https://github.com/rzk-lang/rzk/pull/114))
+
+Fixes:
+
+- Fix error messages in Rzk Playground (see [#115](https://github.com/rzk-lang/rzk/pull/115))
+
 ## v0.6.4 — 2023-09-27
 
 This version improves the stucture of the project, in particular w.r.t dependencies:
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,29 @@
-import Distribution.Simple
-main = defaultMain
+-- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262
+
+-- | Custom Setup that runs bnfc to generate the language sub-libraries
+-- for the parsers included in Ogma.
+module Main (main) where
+
+import           Distribution.Simple         (defaultMainWithHooks,
+                                              hookedPrograms, postConf,
+                                              preBuild, simpleUserHooks)
+import           Distribution.Simple.Program (Program (..), findProgramVersion,
+                                              simpleProgram)
+import           System.Process              (system)
+
+-- | Run BNFC on the grammar before the actual build step.
+--
+-- All options for bnfc are hard-coded here.
+main :: IO ()
+main = defaultMainWithHooks $ simpleUserHooks
+  { hookedPrograms = [ bnfcProgram ]
+  , postConf       = \args flags packageDesc localBuildInfo -> do
+      _ <- system "bnfc -d -p Language.Rzk --generic --functor -o src/ grammar/Syntax.cf"
+      postConf simpleUserHooks args flags packageDesc localBuildInfo
+  }
+
+-- | TODO: This should be in Cabal.Distribution.Simple.Program.Builtin.
+bnfcProgram :: Program
+bnfcProgram = (simpleProgram "bnfc")
+  { programFindVersion = findProgramVersion "--version" id
+  }
diff --git a/grammar/Syntax.cf b/grammar/Syntax.cf
new file mode 100644
--- /dev/null
+++ b/grammar/Syntax.cf
@@ -0,0 +1,164 @@
+comment "--" ;
+comment "{-" "-}" ;
+
+layout toplevel ;
+
+token VarIdentToken ((char - ["-?!.\\;,#\"][)(}{><| \t\n\r"]) (char - ["\\;,#\"][)(}{><| \t\n\r"])*) ;
+
+token HoleIdentToken '?' ;
+
+Module. Module ::= LanguageDecl [Command] ;
+
+HoleIdent. HoleIdent ::= HoleIdentToken ;
+
+VarIdent. VarIdent ::= VarIdentToken ;
+separator nonempty VarIdent "" ;
+
+LanguageDecl. LanguageDecl ::= "#lang" Language ";" ;
+
+Rzk1. Language ::= "rzk-1" ;
+
+CommandSetOption.         Command ::= "#set-option" String "=" String ;
+CommandUnsetOption.       Command ::= "#unset-option" String ;
+
+CommandCheck.             Command ::= "#check" Term ":" Term ;
+
+CommandCompute.           Command ::= "#compute" Term ;
+CommandComputeWHNF.       Command ::= "#compute-whnf" Term ;
+CommandComputeNF.         Command ::= "#compute-nf" Term ;
+
+CommandPostulate.         Command ::= "#postulate" VarIdent DeclUsedVars [Param] ":" Term ;
+commandPostulateNoParams. Command ::= "#postulate" VarIdent DeclUsedVars ":" Term ;
+define commandPostulateNoParams x vars ty = CommandPostulate x vars [] ty ;
+
+CommandAssume.            Command ::= "#assume" [VarIdent] ":" Term ;
+commandVariable.          Command ::= "#variable" VarIdent ":" Term ;
+define commandVariable name term = CommandAssume [name] term ;
+commandVariables.         Command ::= "#variables" [VarIdent] ":" Term ;
+define commandVariables names term = CommandAssume names term ;
+
+CommandSection.           Command ::= "#section" SectionName ;
+CommandSectionEnd.        Command ::= "#end" SectionName ;
+
+CommandDefine.            Command ::= "#define" VarIdent DeclUsedVars [Param] ":" Term ":=" Term ;
+commandDefineNoParams.    Command ::= "#define" VarIdent DeclUsedVars ":" Term ":=" Term ;
+define commandDefineNoParams x vars ty term = CommandDefine x vars [] ty term ;
+commandDef.               Command ::= "#def" VarIdent DeclUsedVars [Param] ":" Term ":=" Term ;
+define commandDef x vars params ty term = CommandDefine x vars params ty term ;
+commandDefNoParams.       Command ::= "#def" VarIdent DeclUsedVars ":" Term ":=" Term ;
+define commandDefNoParams x vars ty term = CommandDefine x vars [] ty term ;
+terminator Command ";" ;
+
+DeclUsedVars. DeclUsedVars ::= "uses" "(" [VarIdent] ")" ;
+noDeclUsedVars. DeclUsedVars ::= ;
+define noDeclUsedVars = DeclUsedVars [] ;
+
+NoSectionName.    SectionName ::= ;
+SomeSectionName.  SectionName ::= VarIdent ;
+
+-- Patterns
+PatternUnit.      Pattern ::= "unit" ;
+PatternVar.       Pattern ::= VarIdent ;
+PatternPair.      Pattern ::= "(" Pattern "," Pattern ")" ;
+separator nonempty Pattern "" ;
+
+-- Parameter introduction (for lambda abstractions)
+ParamPattern.      Param ::= Pattern ;
+ParamPatternType.  Param ::= "(" [Pattern] ":" Term ")" ;
+ParamPatternShape. Param ::= "(" [Pattern] ":" Term "|" Term ")" ;
+ParamPatternShapeDeprecated. Param ::= "{" Pattern ":" Term "|" Term "}" ;
+separator nonempty Param "" ;
+
+-- Parameter declaration for functions and extension types
+ParamType.          ParamDecl ::= Term6 ;
+ParamTermType.      ParamDecl ::= "(" Term ":" Term ")" ;
+ParamTermShape.     ParamDecl ::= "(" Term ":" Term "|" Term ")" ;
+ParamTermTypeDeprecated. ParamDecl ::= "{" Pattern ":" Term "}" ;
+ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}" ;
+paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;
+define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;
+
+Restriction. Restriction ::= Term "↦" Term ;
+separator nonempty Restriction "," ;
+
+-- Universes
+Universe.       Term7 ::= "U" ;
+UniverseCube.   Term7 ::= "CUBE" ;
+UniverseTope.   Term7 ::= "TOPE" ;
+-- Cubes
+CubeUnit.       Term7 ::= "1" ;
+CubeUnitStar.   Term7 ::= "*₁" ;
+Cube2.          Term7 ::= "2" ;
+Cube2_0.        Term7 ::= "0₂" ;
+Cube2_1.        Term7 ::= "1₂" ;
+CubeProduct.    Term5 ::= Term5 "×" Term6 ;
+-- Topes
+TopeTop.        Term7 ::= "⊤" ;
+TopeBottom.     Term7 ::= "⊥" ;
+TopeEQ.         Term4 ::= Term5 "≡" Term5 ;
+TopeLEQ.        Term4 ::= Term5 "≤" Term5 ;
+TopeAnd.        Term3 ::= Term4 "∧" Term3 ;
+TopeOr.         Term2 ::= Term3 "∨" Term2 ;
+-- Tope disjunction elimination
+RecBottom.        Term7 ::= "recBOT" ;
+RecOr.            Term7 ::= "recOR" "(" [Restriction] ")" ;
+RecOrDeprecated.  Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ;
+-- Types
+TypeFun.        Term1 ::= ParamDecl "→" Term1 ;
+TypeSigma.      Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;
+TypeUnit.       Term7 ::= "Unit" ;
+TypeId.         Term1 ::= Term2 "=_{" Term "}" Term2 ;
+TypeIdSimple.   Term1 ::= Term2 "=" Term2 ;
+TypeRestricted. Term6  ::= Term6 "[" [Restriction] "]" ;
+TypeExtensionDeprecated.  Term7 ::= "<" ParamDecl "→" Term ">" ;
+-- Terms
+App.            Term6 ::= Term6 Term7 ;
+Lambda.         Term1 ::= "\\" [Param] "→" Term1 ;
+Pair.           Term7 ::= "(" Term "," Term ")" ;
+First.          Term6 ::= "π₁" Term7 ;
+Second.         Term6 ::= "π₂" Term7 ;
+Unit.           Term7 ::= "unit" ;
+Refl.           Term7 ::= "refl";
+ReflTerm.       Term7 ::= "refl_{" Term "}" ;
+ReflTermType.   Term7 ::= "refl_{" Term ":" Term "}" ;
+IdJ.            Term7 ::= "idJ" "(" Term "," Term "," Term "," Term "," Term "," Term ")" ;
+-- Variables and holes
+Hole.           Term7 ::= HoleIdent;
+Var.            Term7 ::= VarIdent ;
+-- Miscellaneous
+TypeAsc.        Term ::= Term2 "as" Term1 ;
+
+separator nonempty Term "," ;
+coercions Term 7 ;
+
+-- ASCII version of some rules above
+
+ascii_CubeProduct.    Term5 ::= Term5 "*" Term6 ;
+define ascii_CubeProduct l r = CubeProduct l r ;
+
+ASCII_CubeUnitStar.   Term7 ::= "*_1" ;
+ASCII_Cube2_0.        Term7 ::= "0_2" ;
+ASCII_Cube2_1.        Term7 ::= "1_2" ;
+
+ASCII_TopeTop.        Term7 ::= "TOP" ;
+ASCII_TopeBottom.     Term7 ::= "BOT" ;
+ASCII_TopeEQ.         Term4 ::= Term5 "===" Term5 ;
+ASCII_TopeLEQ.        Term4 ::= Term5 "<=" Term5 ;
+ASCII_TopeAnd.        Term3 ::= Term4 "/\\" Term3 ;
+ASCII_TopeOr.         Term2 ::= Term3 "\\/" Term2 ;
+
+ASCII_TypeFun.        Term1 ::= ParamDecl "->" Term1 ;
+ASCII_TypeSigma.      Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;
+
+ASCII_Lambda.         Term1 ::= "\\" [Param] "->" Term1 ;
+ASCII_Restriction. Restriction ::= Term "|->" Term ;
+
+ASCII_TypeExtensionDeprecated.  Term7 ::= "<" ParamDecl "->" Term ">" ;
+
+ASCII_First.          Term6 ::= "first" Term7 ;
+ASCII_Second.         Term6 ::= "second" Term7 ;
+
+-- Alternative Unicode syntax rules
+
+unicode_TypeSigmaAlt.   Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ;    -- \sum
+define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -1,11 +1,11 @@
-cabal-version: 1.12
+cabal-version: 1.24
 
--- This file has been generated from package.yaml by hpack version 0.35.2.
+-- This file has been generated from package.yaml by hpack version 0.36.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.6.4
+version:        0.6.5
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -16,17 +16,24 @@
 copyright:      2023 Nikolai Kudasov
 license:        BSD3
 license-file:   LICENSE
-build-type:     Simple
+build-type:     Custom
 extra-source-files:
     README.md
     ChangeLog.md
+    grammar/Syntax.cf
 
 source-repository head
   type: git
   location: https://github.com/rzk-lang/rzk
 
+custom-setup
+  setup-depends:
+      Cabal >=2.4.0.1 && <4.0
+    , base >=4.11.0.0 && <5.0
+    , process >=1.6.3.0
+
 flag lsp
-  description: Build with LSP support.
+  description: Build with LSP support (only available with GHC, not GHCJS).
   manual: True
   default: True
 
@@ -43,6 +50,7 @@
       Language.Rzk.Syntax.Print
       Rzk
       Rzk.Main
+      Rzk.Project.Config
       Rzk.TypeCheck
   other-modules:
       Paths_rzk
@@ -52,19 +60,17 @@
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob >=0.9.3
-    , aeson >=1.4.2.0
     , array >=0.5.3.0
     , base >=4.7 && <5
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
-    , data-default-class >=0.1.2.0
-    , filepath >=1.4.2.1
-    , lens >=4.17
+    , directory >=1.2.7.0
     , mtl >=2.2.2
     , optparse-generic >=1.3.0
-    , stm >=2.5.0.0
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
     , yaml >=0.11.0.0
@@ -74,11 +80,18 @@
         Language.Rzk.VSCode.Env
         Language.Rzk.VSCode.Handlers
         Language.Rzk.VSCode.Lsp
-        Language.Rzk.VSCode.State
         Language.Rzk.VSCode.Tokenize
+        Language.Rzk.VSCode.Logging
+    cpp-options: -DLSP
     build-depends:
-        lsp >=2.1.0.0
-      , lsp-types >=2.0.1.0
+        aeson >=1.4.2.0
+      , co-log-core >=0.3.2.0
+      , data-default-class >=0.1.2.0
+      , filepath >=1.4.2.1
+      , lens >=4.17
+      , lsp >=2.2.0.0
+      , lsp-types >=2.0.2.0
+      , stm >=2.5.0.0
 
 executable rzk
   main-is: Main.hs
@@ -90,25 +103,23 @@
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob >=0.9.3
-    , aeson >=1.4.2.0
     , array >=0.5.3.0
     , base >=4.7 && <5
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
-    , data-default-class >=0.1.2.0
-    , filepath >=1.4.2.1
-    , lens >=4.17
+    , directory >=1.2.7.0
     , mtl >=2.2.2
     , optparse-generic >=1.3.0
     , rzk
-    , stm >=2.5.0.0
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
     , yaml >=0.11.0.0
   default-language: Haskell2010
-  if flag(lsp) && !impl(ghcjs)
+  if !impl(ghcjs)
     build-depends:
         with-utf8 >=1.0.2.4
 
@@ -121,21 +132,19 @@
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob
     , QuickCheck
-    , aeson >=1.4.2.0
     , array >=0.5.3.0
     , base
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
-    , data-default-class >=0.1.2.0
+    , directory >=1.2.7.0
     , doctest
-    , filepath >=1.4.2.1
-    , lens >=4.17
     , mtl >=2.2.2
     , optparse-generic >=1.3.0
-    , stm >=2.5.0.0
     , template-haskell
     , text >=1.2.3.1
     , yaml >=0.11.0.0
@@ -152,20 +161,18 @@
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob >=0.9.3
-    , aeson >=1.4.2.0
     , array >=0.5.3.0
     , base >=4.7 && <5
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
-    , data-default-class >=0.1.2.0
-    , filepath >=1.4.2.1
-    , lens >=4.17
+    , directory >=1.2.7.0
     , mtl >=2.2.2
     , optparse-generic >=1.3.0
     , rzk
-    , stm >=2.5.0.0
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
     , yaml >=0.11.0.0
diff --git a/src/Language/Rzk/Free/Syntax.hs b/src/Language/Rzk/Free/Syntax.hs
--- a/src/Language/Rzk/Free/Syntax.hs
+++ b/src/Language/Rzk/Free/Syntax.hs
@@ -94,7 +94,7 @@
     | TypeUnitF
     | TypeAscF term term
     | TypeRestrictedF term [(term, term)]
-    deriving (Eq)
+    deriving (Eq, Functor, Foldable, Traversable)
 deriveBifunctor ''TermF
 deriveBifoldable ''TermF
 deriveBitraversable ''TermF
diff --git a/src/Language/Rzk/Syntax.hs b/src/Language/Rzk/Syntax.hs
--- a/src/Language/Rzk/Syntax.hs
+++ b/src/Language/Rzk/Syntax.hs
@@ -9,7 +9,7 @@
   parseModuleRzk,
   parseModuleFile,
   parseTerm,
-  printTree,
+  Print.Print(..), printTree,
   tryExtractMarkdownCodeBlocks,
   extractMarkdownCodeBlocks,
   tryOrDisplayException,
@@ -23,7 +23,7 @@
 import qualified Data.List                  as List
 
 import           Language.Rzk.Syntax.Abs
-import           Language.Rzk.Syntax.Print  (printTree)
+import qualified Language.Rzk.Syntax.Print  as Print
 
 import           Language.Rzk.Syntax.Layout (resolveLayout)
 import           Language.Rzk.Syntax.Lex    (tokens)
@@ -121,3 +121,69 @@
   | otherwise = NonCode
   where
     (prefix, suffix) = List.splitAt 3 line
+
+-- * Overriding BNFC pretty-printer
+
+-- | Like 'Print.printTree', but does not insert newlines for curly braces.
+printTree :: Print.Print a => a -> String
+printTree = render . Print.prt 0
+
+-- | Like 'Print.render', but does not insert newlines for curly braces.
+render :: Print.Doc -> String
+render d = rend 0 False (map ($ "") $ d []) ""
+  where
+  rend
+    :: Int        -- ^ Indentation level.
+    -> Bool       -- ^ Pending indentation to be output before next character?
+    -> [String]
+    -> ShowS
+  rend i p = \case
+      "["      :ts -> char '[' . rend i False ts
+      "("      :ts -> char '(' . rend i False ts
+      -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
+      -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
+      -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
+      [";"]        -> char ';'
+      ";"      :ts -> char ';' . new i ts
+      t  : ts@(s:_) | closingOrPunctuation s
+                   -> pending . showString t . rend i False ts
+      t        :ts -> pending . space t      . rend i False ts
+      []           -> id
+    where
+    -- Output character after pending indentation.
+    char :: Char -> ShowS
+    char c = pending . showChar c
+
+    -- Output pending indentation.
+    pending :: ShowS
+    pending = if p then indent i else id
+
+  -- Indentation (spaces) for given indentation level.
+  indent :: Int -> ShowS
+  indent i = Print.replicateS (2*i) (showChar ' ')
+
+  -- Continue rendering in new line with new indentation.
+  new :: Int -> [String] -> ShowS
+  new j ts = showChar '\n' . rend j True ts
+
+  -- -- Make sure we are on a fresh line.
+  -- onNewLine :: Int -> Bool -> ShowS
+  -- onNewLine i p = (if p then id else showChar '\n') . indent i
+
+  -- Separate given string from following text by a space (if needed).
+  space :: String -> ShowS
+  space t s =
+    case (all isSpace t, null spc, null rest) of
+      (True , _   , True ) -> []             -- remove trailing space
+      (False, _   , True ) -> t              -- remove trailing space
+      (False, True, False) -> t ++ ' ' : s   -- add space if none
+      _                    -> t ++ s
+    where
+      (spc, rest) = span isSpace s
+
+  closingOrPunctuation :: String -> Bool
+  closingOrPunctuation [c] = c `elem` closerOrPunct
+  closingOrPunctuation _   = False
+
+  closerOrPunct :: String
+  closerOrPunct = ")],;"
diff --git a/src/Language/Rzk/Syntax/Abs.hs b/src/Language/Rzk/Syntax/Abs.hs
--- a/src/Language/Rzk/Syntax/Abs.hs
+++ b/src/Language/Rzk/Syntax/Abs.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
diff --git a/src/Language/Rzk/Syntax/Layout.hs b/src/Language/Rzk/Syntax/Layout.hs
--- a/src/Language/Rzk/Syntax/Layout.hs
+++ b/src/Language/Rzk/Syntax/Layout.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 
diff --git a/src/Language/Rzk/Syntax/Lex.x b/src/Language/Rzk/Syntax/Lex.x
new file mode 100644
--- /dev/null
+++ b/src/Language/Rzk/Syntax/Lex.x
@@ -0,0 +1,292 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+
+-- Lexer definition for use with Alex 3
+{
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+{-# OPTIONS_GHC -w #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+
+module Language.Rzk.Syntax.Lex where
+
+import Prelude
+
+import qualified Data.Bits
+import Data.Char     (ord)
+import Data.Function (on)
+import Data.Word     (Word8)
+}
+
+-- Predefined character classes
+
+$c = [A-Z\192-\221] # [\215]  -- capital isolatin1 letter (215 = \times) FIXME
+$s = [a-z\222-\255] # [\247]  -- small   isolatin1 letter (247 = \div  ) FIXME
+$l = [$c $s]         -- letter
+$d = [0-9]           -- digit
+$i = [$l $d _ ']     -- identifier character
+$u = [. \n]          -- universal: any character
+
+-- Symbols and non-identifier-like reserved words
+
+@rsyms = \Σ | \π \₁ | \π \₂ | \# "lang" | \; | "rzk" \- "1" | \# "set" \- "option" | \= | \# "unset" \- "option" | \# "check" | \: | \# "compute" | \# "compute" \- "whnf" | \# "compute" \- "nf" | \# "postulate" | \# "assume" | \# "variable" | \# "variables" | \# "section" | \# "end" | \# "define" | \: \= | \# "def" | \( | \) | \, | \| | \{ | \} | \↦ | "1" | \* \₁ | "2" | "0" \₂ | "1" \₂ | \× | \⊤ | \⊥ | \≡ | \≤ | \∧ | \∨ | \→ | \= \_ \{ | \[ | \] | \< | \> | \\ | "refl" \_ \{ | \* | \* \_ "1" | "0" \_ "2" | "1" \_ "2" | \= \= \= | \< \= | \/ \\ | \\ \/ | \- \> | \| \- \> | \∑
+
+:-
+
+-- Line comment "--"
+"--" [.]* ;
+
+-- Block comment "{-" "-}"
+\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;
+
+-- Whitespace (skipped)
+$white+ ;
+
+-- Symbols
+@rsyms
+    { tok (eitherResIdent TV) }
+
+-- token VarIdentToken
+[$u # [\t \n \r \  \! \" \# \( \) \, \- \. \; \< \> \? \[ \\ \] \{ \| \}]] [$u # [\t \n \r \  \" \# \( \) \, \; \< \> \[ \\ \] \{ \| \}]] *
+    { tok (eitherResIdent T_VarIdentToken) }
+
+-- token HoleIdentToken
+\?
+    { tok (eitherResIdent T_HoleIdentToken) }
+
+-- Keywords and Ident
+$l $i*
+    { tok (eitherResIdent TV) }
+
+-- String
+\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \"
+    { tok (TL . unescapeInitTail) }
+
+{
+-- | Create a token with position.
+tok :: (String -> Tok) -> (Posn -> String -> Token)
+tok f p = PT p . f
+
+-- | Token without position.
+data Tok
+  = TK {-# UNPACK #-} !TokSymbol  -- ^ Reserved word or symbol.
+  | TL !String                    -- ^ String literal.
+  | TI !String                    -- ^ Integer literal.
+  | TV !String                    -- ^ Identifier.
+  | TD !String                    -- ^ Float literal.
+  | TC !String                    -- ^ Character literal.
+  | T_VarIdentToken !String
+  | T_HoleIdentToken !String
+  deriving (Eq, Show, Ord)
+
+-- | Smart constructor for 'Tok' for the sake of backwards compatibility.
+pattern TS :: String -> Int -> Tok
+pattern TS t i = TK (TokSymbol t i)
+
+-- | Keyword or symbol tokens have a unique ID.
+data TokSymbol = TokSymbol
+  { tsText :: String
+      -- ^ Keyword or symbol text.
+  , tsID   :: !Int
+      -- ^ Unique ID.
+  } deriving (Show)
+
+-- | Keyword/symbol equality is determined by the unique ID.
+instance Eq  TokSymbol where (==)    = (==)    `on` tsID
+
+-- | Keyword/symbol ordering is determined by the unique ID.
+instance Ord TokSymbol where compare = compare `on` tsID
+
+-- | Token with position.
+data Token
+  = PT  Posn Tok
+  | Err Posn
+  deriving (Eq, Show, Ord)
+
+-- | Pretty print a position.
+printPosn :: Posn -> String
+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c
+
+-- | Pretty print the position of the first token in the list.
+tokenPos :: [Token] -> String
+tokenPos (t:_) = printPosn (tokenPosn t)
+tokenPos []    = "end of file"
+
+-- | Get the position of a token.
+tokenPosn :: Token -> Posn
+tokenPosn (PT p _) = p
+tokenPosn (Err p)  = p
+
+-- | Get line and column of a token.
+tokenLineCol :: Token -> (Int, Int)
+tokenLineCol = posLineCol . tokenPosn
+
+-- | Get line and column of a position.
+posLineCol :: Posn -> (Int, Int)
+posLineCol (Pn _ l c) = (l,c)
+
+-- | Convert a token into "position token" form.
+mkPosToken :: Token -> ((Int, Int), String)
+mkPosToken t = (tokenLineCol t, tokenText t)
+
+-- | Convert a token to its text.
+tokenText :: Token -> String
+tokenText t = case t of
+  PT _ (TS s _) -> s
+  PT _ (TL s)   -> show s
+  PT _ (TI s)   -> s
+  PT _ (TV s)   -> s
+  PT _ (TD s)   -> s
+  PT _ (TC s)   -> s
+  Err _         -> "#error"
+  PT _ (T_VarIdentToken s) -> s
+  PT _ (T_HoleIdentToken s) -> s
+
+-- | Convert a token to a string.
+prToken :: Token -> String
+prToken t = tokenText t
+
+-- | Finite map from text to token organized as binary search tree.
+data BTree
+  = N -- ^ Nil (leaf).
+  | B String Tok BTree BTree
+      -- ^ Binary node.
+  deriving (Show)
+
+-- | Convert potential keyword into token or use fallback conversion.
+eitherResIdent :: (String -> Tok) -> String -> Tok
+eitherResIdent tv s = treeFind resWords
+  where
+  treeFind N = tv s
+  treeFind (B a t left right) =
+    case compare s a of
+      LT -> treeFind left
+      GT -> treeFind right
+      EQ -> t
+
+-- | The keywords and symbols of the language organized as binary search tree.
+resWords :: BTree
+resWords =
+  b "BOT" 39
+    (b "*\8321" 20
+       (b "#postulate" 10
+          (b "#compute-whnf" 5
+             (b "#compute" 3
+                (b "#check" 2 (b "#assume" 1 N N) N) (b "#compute-nf" 4 N N))
+             (b "#end" 8 (b "#define" 7 (b "#def" 6 N N) N) (b "#lang" 9 N N)))
+          (b "#variables" 15
+             (b "#unset-option" 13
+                (b "#set-option" 12 (b "#section" 11 N N) N)
+                (b "#variable" 14 N N))
+             (b "*" 18 (b ")" 17 (b "(" 16 N N) N) (b "*_1" 19 N N))))
+       (b ":" 30
+          (b "0\8322" 25
+             (b "/\\" 23 (b "->" 22 (b "," 21 N N) N) (b "0_2" 24 N N))
+             (b "1\8322" 28 (b "1_2" 27 (b "1" 26 N N) N) (b "2" 29 N N)))
+          (b "=" 35
+             (b "<" 33 (b ";" 32 (b ":=" 31 N N) N) (b "<=" 34 N N))
+             (b "=_{" 37 (b "===" 36 N N) (b ">" 38 N N)))))
+    (b "unit" 59
+       (b "]" 49
+          (b "U" 44
+             (b "TOP" 42 (b "Sigma" 41 (b "CUBE" 40 N N) N) (b "TOPE" 43 N N))
+             (b "\\" 47 (b "[" 46 (b "Unit" 45 N N) N) (b "\\/" 48 N N)))
+          (b "recOR" 54
+             (b "idJ" 52 (b "first" 51 (b "as" 50 N N) N) (b "recBOT" 53 N N))
+             (b "rzk-1" 57
+                (b "refl_{" 56 (b "refl" 55 N N) N) (b "second" 58 N N))))
+       (b "\8594" 69
+          (b "}" 64
+             (b "|" 62 (b "{" 61 (b "uses" 60 N N) N) (b "|->" 63 N N))
+             (b "\960\8321" 67
+                (b "\931" 66 (b "\215" 65 N N) N) (b "\960\8322" 68 N N)))
+          (b "\8801" 74
+             (b "\8743" 72
+                (b "\8721" 71 (b "\8614" 70 N N) N) (b "\8744" 73 N N))
+             (b "\8868" 76 (b "\8804" 75 N N) (b "\8869" 77 N N)))))
+  where
+  b s n = B bs (TS bs n)
+    where
+    bs = s
+
+-- | Unquote string literal.
+unescapeInitTail :: String -> String
+unescapeInitTail = id . unesc . tail . id
+  where
+  unesc s = case s of
+    '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs
+    '\\':'n':cs  -> '\n' : unesc cs
+    '\\':'t':cs  -> '\t' : unesc cs
+    '\\':'r':cs  -> '\r' : unesc cs
+    '\\':'f':cs  -> '\f' : unesc cs
+    '"':[]       -> []
+    c:cs         -> c : unesc cs
+    _            -> []
+
+-------------------------------------------------------------------
+-- Alex wrapper code.
+-- A modified "posn" wrapper.
+-------------------------------------------------------------------
+
+data Posn = Pn !Int !Int !Int
+  deriving (Eq, Show, Ord)
+
+alexStartPos :: Posn
+alexStartPos = Pn 0 1 1
+
+alexMove :: Posn -> Char -> Posn
+alexMove (Pn a l c) '\t' = Pn (a+1)  l     (((c+7) `div` 8)*8+1)
+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1)   1
+alexMove (Pn a l c) _    = Pn (a+1)  l     (c+1)
+
+type Byte = Word8
+
+type AlexInput = (Posn,     -- current position,
+                  Char,     -- previous char
+                  [Byte],   -- pending bytes on the current char
+                  String)   -- current input string
+
+tokens :: String -> [Token]
+tokens str = go (alexStartPos, '\n', [], str)
+    where
+      go :: AlexInput -> [Token]
+      go inp@(pos, _, _, str) =
+               case alexScan inp 0 of
+                AlexEOF                   -> []
+                AlexError (pos, _, _, _)  -> [Err pos]
+                AlexSkip  inp' len        -> go inp'
+                AlexToken inp' len act    -> act pos (take len str) : (go inp')
+
+alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)
+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))
+alexGetByte (p, _, [], s) =
+  case s of
+    []  -> Nothing
+    (c:s) ->
+             let p'     = alexMove p c
+                 (b:bs) = utf8Encode c
+              in p' `seq` Just (b, (p', c, bs, s))
+
+alexInputPrevChar :: AlexInput -> Char
+alexInputPrevChar (p, c, bs, s) = c
+
+-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.
+utf8Encode :: Char -> [Word8]
+utf8Encode = map fromIntegral . go . ord
+  where
+  go oc
+   | oc <= 0x7f       = [oc]
+
+   | oc <= 0x7ff      = [ 0xc0 + (oc `Data.Bits.shiftR` 6)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+
+   | oc <= 0xffff     = [ 0xe0 + (oc `Data.Bits.shiftR` 12)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+   | otherwise        = [ 0xf0 + (oc `Data.Bits.shiftR` 18)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)
+                        , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)
+                        , 0x80 + oc Data.Bits..&. 0x3f
+                        ]
+}
diff --git a/src/Language/Rzk/Syntax/Par.y b/src/Language/Rzk/Syntax/Par.y
new file mode 100644
--- /dev/null
+++ b/src/Language/Rzk/Syntax/Par.y
@@ -0,0 +1,457 @@
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
+
+-- Parser definition for use with Happy
+{
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Language.Rzk.Syntax.Par
+  ( happyError
+  , myLexer
+  , pModule
+  , pHoleIdent
+  , pVarIdent
+  , pListVarIdent
+  , pLanguageDecl
+  , pLanguage
+  , pCommand
+  , pListCommand
+  , pDeclUsedVars
+  , pSectionName
+  , pPattern
+  , pListPattern
+  , pParam
+  , pListParam
+  , pParamDecl
+  , pRestriction
+  , pListRestriction
+  , pTerm7
+  , pTerm5
+  , pTerm4
+  , pTerm3
+  , pTerm2
+  , pTerm1
+  , pTerm6
+  , pTerm
+  , pListTerm
+  ) where
+
+import Prelude
+
+import qualified Language.Rzk.Syntax.Abs
+import Language.Rzk.Syntax.Lex
+
+}
+
+%name pModule_internal Module
+%name pHoleIdent_internal HoleIdent
+%name pVarIdent_internal VarIdent
+%name pListVarIdent_internal ListVarIdent
+%name pLanguageDecl_internal LanguageDecl
+%name pLanguage_internal Language
+%name pCommand_internal Command
+%name pListCommand_internal ListCommand
+%name pDeclUsedVars_internal DeclUsedVars
+%name pSectionName_internal SectionName
+%name pPattern_internal Pattern
+%name pListPattern_internal ListPattern
+%name pParam_internal Param
+%name pListParam_internal ListParam
+%name pParamDecl_internal ParamDecl
+%name pRestriction_internal Restriction
+%name pListRestriction_internal ListRestriction
+%name pTerm7_internal Term7
+%name pTerm5_internal Term5
+%name pTerm4_internal Term4
+%name pTerm3_internal Term3
+%name pTerm2_internal Term2
+%name pTerm1_internal Term1
+%name pTerm6_internal Term6
+%name pTerm_internal Term
+%name pListTerm_internal ListTerm
+-- no lexer declaration
+%monad { Err } { (>>=) } { return }
+%tokentype {Token}
+%token
+  '#assume'        { PT _ (TS _ 1)             }
+  '#check'         { PT _ (TS _ 2)             }
+  '#compute'       { PT _ (TS _ 3)             }
+  '#compute-nf'    { PT _ (TS _ 4)             }
+  '#compute-whnf'  { PT _ (TS _ 5)             }
+  '#def'           { PT _ (TS _ 6)             }
+  '#define'        { PT _ (TS _ 7)             }
+  '#end'           { PT _ (TS _ 8)             }
+  '#lang'          { PT _ (TS _ 9)             }
+  '#postulate'     { PT _ (TS _ 10)            }
+  '#section'       { PT _ (TS _ 11)            }
+  '#set-option'    { PT _ (TS _ 12)            }
+  '#unset-option'  { PT _ (TS _ 13)            }
+  '#variable'      { PT _ (TS _ 14)            }
+  '#variables'     { PT _ (TS _ 15)            }
+  '('              { PT _ (TS _ 16)            }
+  ')'              { PT _ (TS _ 17)            }
+  '*'              { PT _ (TS _ 18)            }
+  '*_1'            { PT _ (TS _ 19)            }
+  '*₁'             { PT _ (TS _ 20)            }
+  ','              { PT _ (TS _ 21)            }
+  '->'             { PT _ (TS _ 22)            }
+  '/\\'            { PT _ (TS _ 23)            }
+  '0_2'            { PT _ (TS _ 24)            }
+  '0₂'             { PT _ (TS _ 25)            }
+  '1'              { PT _ (TS _ 26)            }
+  '1_2'            { PT _ (TS _ 27)            }
+  '1₂'             { PT _ (TS _ 28)            }
+  '2'              { PT _ (TS _ 29)            }
+  ':'              { PT _ (TS _ 30)            }
+  ':='             { PT _ (TS _ 31)            }
+  ';'              { PT _ (TS _ 32)            }
+  '<'              { PT _ (TS _ 33)            }
+  '<='             { PT _ (TS _ 34)            }
+  '='              { PT _ (TS _ 35)            }
+  '==='            { PT _ (TS _ 36)            }
+  '=_{'            { PT _ (TS _ 37)            }
+  '>'              { PT _ (TS _ 38)            }
+  'BOT'            { PT _ (TS _ 39)            }
+  'CUBE'           { PT _ (TS _ 40)            }
+  'Sigma'          { PT _ (TS _ 41)            }
+  'TOP'            { PT _ (TS _ 42)            }
+  'TOPE'           { PT _ (TS _ 43)            }
+  'U'              { PT _ (TS _ 44)            }
+  'Unit'           { PT _ (TS _ 45)            }
+  '['              { PT _ (TS _ 46)            }
+  '\\'             { PT _ (TS _ 47)            }
+  '\\/'            { PT _ (TS _ 48)            }
+  ']'              { PT _ (TS _ 49)            }
+  'as'             { PT _ (TS _ 50)            }
+  'first'          { PT _ (TS _ 51)            }
+  'idJ'            { PT _ (TS _ 52)            }
+  'recBOT'         { PT _ (TS _ 53)            }
+  'recOR'          { PT _ (TS _ 54)            }
+  'refl'           { PT _ (TS _ 55)            }
+  'refl_{'         { PT _ (TS _ 56)            }
+  'rzk-1'          { PT _ (TS _ 57)            }
+  'second'         { PT _ (TS _ 58)            }
+  'unit'           { PT _ (TS _ 59)            }
+  'uses'           { PT _ (TS _ 60)            }
+  '{'              { PT _ (TS _ 61)            }
+  '|'              { PT _ (TS _ 62)            }
+  '|->'            { PT _ (TS _ 63)            }
+  '}'              { PT _ (TS _ 64)            }
+  '×'              { PT _ (TS _ 65)            }
+  'Σ'              { PT _ (TS _ 66)            }
+  'π₁'             { PT _ (TS _ 67)            }
+  'π₂'             { PT _ (TS _ 68)            }
+  '→'              { PT _ (TS _ 69)            }
+  '↦'              { PT _ (TS _ 70)            }
+  '∑'              { PT _ (TS _ 71)            }
+  '∧'              { PT _ (TS _ 72)            }
+  '∨'              { PT _ (TS _ 73)            }
+  '≡'              { PT _ (TS _ 74)            }
+  '≤'              { PT _ (TS _ 75)            }
+  '⊤'              { PT _ (TS _ 76)            }
+  '⊥'              { PT _ (TS _ 77)            }
+  L_quoted         { PT _ (TL _)               }
+  L_VarIdentToken  { PT _ (T_VarIdentToken _)  }
+  L_HoleIdentToken { PT _ (T_HoleIdentToken _) }
+
+%%
+
+String  :: { (Language.Rzk.Syntax.Abs.BNFC'Position, String) }
+String   : L_quoted { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), ((\(PT _ (TL s)) -> s) $1)) }
+
+VarIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdentToken) }
+VarIdentToken  : L_VarIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.VarIdentToken (tokenText $1)) }
+
+HoleIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdentToken) }
+HoleIdentToken  : L_HoleIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.HoleIdentToken (tokenText $1)) }
+
+Module :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Module) }
+Module
+  : LanguageDecl ListCommand { (fst $1, Language.Rzk.Syntax.Abs.Module (fst $1) (snd $1) (snd $2)) }
+
+HoleIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdent) }
+HoleIdent
+  : HoleIdentToken { (fst $1, Language.Rzk.Syntax.Abs.HoleIdent (fst $1) (snd $1)) }
+
+VarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdent) }
+VarIdent
+  : VarIdentToken { (fst $1, Language.Rzk.Syntax.Abs.VarIdent (fst $1) (snd $1)) }
+
+ListVarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.VarIdent]) }
+ListVarIdent
+  : VarIdent { (fst $1, (:[]) (snd $1)) }
+  | VarIdent ListVarIdent { (fst $1, (:) (snd $1) (snd $2)) }
+
+LanguageDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.LanguageDecl) }
+LanguageDecl
+  : '#lang' Language ';' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.LanguageDecl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+
+Language :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Language) }
+Language
+  : 'rzk-1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Rzk1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+
+Command :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Command) }
+Command
+  : '#set-option' String '=' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#unset-option' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandUnsetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#check' Term ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCheck (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#compute' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCompute (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#compute-whnf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeWHNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#compute-nf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#postulate' VarIdent DeclUsedVars ListParam ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandPostulate (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6)) }
+  | '#postulate' VarIdent DeclUsedVars ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandPostulateNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5)) }
+  | '#assume' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandAssume (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#variable' VarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariable (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#variables' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariables (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '#section' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSection (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#end' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSectionEnd (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | '#define' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandDefine (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }
+  | '#define' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefineNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }
+  | '#def' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDef (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }
+  | '#def' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }
+
+ListCommand :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Command]) }
+ListCommand
+  : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, []) }
+  | Command ';' ListCommand { (fst $1, (:) (snd $1) (snd $3)) }
+
+DeclUsedVars :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.DeclUsedVars) }
+DeclUsedVars
+  : 'uses' '(' ListVarIdent ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.DeclUsedVars (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }
+  | {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.noDeclUsedVars Language.Rzk.Syntax.Abs.BNFC'NoPosition) }
+
+SectionName :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SectionName) }
+SectionName
+  : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.NoSectionName Language.Rzk.Syntax.Abs.BNFC'NoPosition) }
+  | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.SomeSectionName (fst $1) (snd $1)) }
+
+Pattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Pattern) }
+Pattern
+  : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) }
+  | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+
+ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }
+ListPattern
+  : Pattern { (fst $1, (:[]) (snd $1)) }
+  | Pattern ListPattern { (fst $1, (:) (snd $1) (snd $2)) }
+
+Param :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Param) }
+Param
+  : Pattern { (fst $1, Language.Rzk.Syntax.Abs.ParamPattern (fst $1) (snd $1)) }
+  | '(' ListPattern ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' ListPattern ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+  | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+
+ListParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Param]) }
+ListParam
+  : Param { (fst $1, (:[]) (snd $1)) }
+  | Param ListParam { (fst $1, (:) (snd $1) (snd $2)) }
+
+ParamDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.ParamDecl) }
+ParamDecl
+  : Term6 { (fst $1, Language.Rzk.Syntax.Abs.ParamType (fst $1) (snd $1)) }
+  | '(' Term ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Term ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+  | '{' Pattern ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '{' '(' Pattern ':' Term ')' '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.paramVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
+
+Restriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Restriction) }
+Restriction
+  : Term '↦' Term { (fst $1, Language.Rzk.Syntax.Abs.Restriction (fst $1) (snd $1) (snd $3)) }
+  | Term '|->' Term { (fst $1, Language.Rzk.Syntax.Abs.ASCII_Restriction (fst $1) (snd $1) (snd $3)) }
+
+ListRestriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Restriction]) }
+ListRestriction
+  : Restriction { (fst $1, (:[]) (snd $1)) }
+  | Restriction ',' ListRestriction { (fst $1, (:) (snd $1) (snd $3)) }
+
+Term7 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term7
+  : 'U' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Universe (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'CUBE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseCube (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'TOPE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseTope (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '*₁' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '0₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '1₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '⊤' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '⊥' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'recBOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'recOR' '(' ListRestriction ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOr (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }
+  | 'recOR' '(' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOrDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9)) }
+  | 'Unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '<' ParamDecl '→' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '(' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Pair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Unit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'refl' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Refl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'refl_{' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTerm (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | 'refl_{' Term ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | 'idJ' '(' Term ',' Term ',' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.IdJ (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9) (snd $11) (snd $13)) }
+  | HoleIdent { (fst $1, Language.Rzk.Syntax.Abs.Hole (fst $1) (snd $1)) }
+  | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.Var (fst $1) (snd $1)) }
+  | '(' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), (snd $2)) }
+  | '*_1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '0_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '1_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'TOP' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | 'BOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }
+  | '<' ParamDecl '->' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+
+Term5 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term5
+  : Term5 '×' Term6 { (fst $1, Language.Rzk.Syntax.Abs.CubeProduct (fst $1) (snd $1) (snd $3)) }
+  | Term6 { (fst $1, (snd $1)) }
+  | Term5 '*' Term6 { (fst $1, Language.Rzk.Syntax.Abs.ascii_CubeProduct (fst $1) (snd $1) (snd $3)) }
+
+Term4 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term4
+  : Term5 '≡' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeEQ (fst $1) (snd $1) (snd $3)) }
+  | Term5 '≤' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeLEQ (fst $1) (snd $1) (snd $3)) }
+  | Term5 { (fst $1, (snd $1)) }
+  | Term5 '===' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeEQ (fst $1) (snd $1) (snd $3)) }
+  | Term5 '<=' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeLEQ (fst $1) (snd $1) (snd $3)) }
+
+Term3 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term3
+  : Term4 '∧' Term3 { (fst $1, Language.Rzk.Syntax.Abs.TopeAnd (fst $1) (snd $1) (snd $3)) }
+  | Term4 { (fst $1, (snd $1)) }
+  | Term4 '/\\' Term3 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeAnd (fst $1) (snd $1) (snd $3)) }
+
+Term2 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term2
+  : Term3 '∨' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TopeOr (fst $1) (snd $1) (snd $3)) }
+  | Term3 { (fst $1, (snd $1)) }
+  | Term3 '\\/' Term2 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeOr (fst $1) (snd $1) (snd $3)) }
+
+Term1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term1
+  : ParamDecl '→' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) }
+  | 'Σ' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | Term2 '=_{' Term '}' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeId (fst $1) (snd $1) (snd $3) (snd $5)) }
+  | Term2 '=' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeIdSimple (fst $1) (snd $1) (snd $3)) }
+  | '\\' ListParam '→' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | Term2 { (fst $1, (snd $1)) }
+  | ParamDecl '->' Term1 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TypeFun (fst $1) (snd $1) (snd $3)) }
+  | 'Sigma' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | '\\' ListParam '->' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
+  | '∑' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+
+Term6 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term6
+  : Term6 '[' ListRestriction ']' { (fst $1, Language.Rzk.Syntax.Abs.TypeRestricted (fst $1) (snd $1) (snd $3)) }
+  | Term6 Term7 { (fst $1, Language.Rzk.Syntax.Abs.App (fst $1) (snd $1) (snd $2)) }
+  | 'π₁' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | 'π₂' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | Term7 { (fst $1, (snd $1)) }
+  | 'first' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+  | 'second' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }
+
+Term :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }
+Term
+  : Term2 'as' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeAsc (fst $1) (snd $1) (snd $3)) }
+  | Term1 { (fst $1, (snd $1)) }
+
+ListTerm :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Term]) }
+ListTerm
+  : Term { (fst $1, (:[]) (snd $1)) }
+  | Term ',' ListTerm { (fst $1, (:) (snd $1) (snd $3)) }
+
+{
+
+type Err = Either String
+
+happyError :: [Token] -> Err a
+happyError ts = Left $
+  "syntax error at " ++ tokenPos ts ++
+  case ts of
+    []      -> []
+    [Err _] -> " due to lexer error"
+    t:_     -> " before `" ++ (prToken t) ++ "'"
+
+myLexer :: String -> [Token]
+myLexer = tokens
+
+-- Entrypoints
+
+pModule :: [Token] -> Err Language.Rzk.Syntax.Abs.Module
+pModule = fmap snd . pModule_internal
+
+pHoleIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.HoleIdent
+pHoleIdent = fmap snd . pHoleIdent_internal
+
+pVarIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.VarIdent
+pVarIdent = fmap snd . pVarIdent_internal
+
+pListVarIdent :: [Token] -> Err [Language.Rzk.Syntax.Abs.VarIdent]
+pListVarIdent = fmap snd . pListVarIdent_internal
+
+pLanguageDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.LanguageDecl
+pLanguageDecl = fmap snd . pLanguageDecl_internal
+
+pLanguage :: [Token] -> Err Language.Rzk.Syntax.Abs.Language
+pLanguage = fmap snd . pLanguage_internal
+
+pCommand :: [Token] -> Err Language.Rzk.Syntax.Abs.Command
+pCommand = fmap snd . pCommand_internal
+
+pListCommand :: [Token] -> Err [Language.Rzk.Syntax.Abs.Command]
+pListCommand = fmap snd . pListCommand_internal
+
+pDeclUsedVars :: [Token] -> Err Language.Rzk.Syntax.Abs.DeclUsedVars
+pDeclUsedVars = fmap snd . pDeclUsedVars_internal
+
+pSectionName :: [Token] -> Err Language.Rzk.Syntax.Abs.SectionName
+pSectionName = fmap snd . pSectionName_internal
+
+pPattern :: [Token] -> Err Language.Rzk.Syntax.Abs.Pattern
+pPattern = fmap snd . pPattern_internal
+
+pListPattern :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]
+pListPattern = fmap snd . pListPattern_internal
+
+pParam :: [Token] -> Err Language.Rzk.Syntax.Abs.Param
+pParam = fmap snd . pParam_internal
+
+pListParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.Param]
+pListParam = fmap snd . pListParam_internal
+
+pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl
+pParamDecl = fmap snd . pParamDecl_internal
+
+pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction
+pRestriction = fmap snd . pRestriction_internal
+
+pListRestriction :: [Token] -> Err [Language.Rzk.Syntax.Abs.Restriction]
+pListRestriction = fmap snd . pListRestriction_internal
+
+pTerm7 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm7 = fmap snd . pTerm7_internal
+
+pTerm5 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm5 = fmap snd . pTerm5_internal
+
+pTerm4 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm4 = fmap snd . pTerm4_internal
+
+pTerm3 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm3 = fmap snd . pTerm3_internal
+
+pTerm2 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm2 = fmap snd . pTerm2_internal
+
+pTerm1 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm1 = fmap snd . pTerm1_internal
+
+pTerm6 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm6 = fmap snd . pTerm6_internal
+
+pTerm :: [Token] -> Err Language.Rzk.Syntax.Abs.Term
+pTerm = fmap snd . pTerm_internal
+
+pListTerm :: [Token] -> Err [Language.Rzk.Syntax.Abs.Term]
+pListTerm = fmap snd . pListTerm_internal
+}
+
diff --git a/src/Language/Rzk/Syntax/Print.hs b/src/Language/Rzk/Syntax/Print.hs
--- a/src/Language/Rzk/Syntax/Print.hs
+++ b/src/Language/Rzk/Syntax/Print.hs
@@ -1,8 +1,8 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
-{-# LANGUAGE CPP                  #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
 #if __GLASGOW_HASKELL__ <= 708
 {-# LANGUAGE OverlappingInstances #-}
 #endif
@@ -11,13 +11,16 @@
 
 module Language.Rzk.Syntax.Print where
 
-import           Data.Char               (Char, isSpace)
+import Prelude
+  ( ($), (.)
+  , Bool(..), (==), (<)
+  , Int, Integer, Double, (+), (-), (*)
+  , String, (++)
+  , ShowS, showChar, showString
+  , all, elem, foldr, id, map, null, replicate, shows, span
+  )
+import Data.Char ( Char, isSpace )
 import qualified Language.Rzk.Syntax.Abs
-import           Prelude                 (Bool (..), Double, Int, Integer,
-                                          ShowS, String, all, elem, foldr, id,
-                                          map, null, replicate, showChar,
-                                          showString, shows, span, ($), (*),
-                                          (++), (.), (<), (==))
 
 -- | The top-level printing method.
 
@@ -40,9 +43,9 @@
   rend i p = \case
       "["      :ts -> char '[' . rend i False ts
       "("      :ts -> char '(' . rend i False ts
-      -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
-      -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
-      -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
+      "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
+      "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
+      "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
       [";"]        -> char ';'
       ";"      :ts -> char ';' . new i ts
       t  : ts@(s:_) | closingOrPunctuation s
@@ -67,19 +70,18 @@
   new j ts = showChar '\n' . rend j True ts
 
   -- Make sure we are on a fresh line.
-  -- onNewLine :: Int -> Bool -> ShowS
-  -- onNewLine i p = (if p then id else showChar '\n') . indent i
+  onNewLine :: Int -> Bool -> ShowS
+  onNewLine i p = (if p then id else showChar '\n') . indent i
 
   -- Separate given string from following text by a space (if needed).
   space :: String -> ShowS
   space t s =
-    case (all isSpace t', null spc, null rest) of
-      (True , _   , True ) -> []              -- remove trailing space
-      (False, _   , True ) -> t'              -- remove trailing space
-      (False, True, False) -> t' ++ ' ' : s   -- add space if none
-      _                    -> t' ++ s
+    case (all isSpace t, null spc, null rest) of
+      (True , _   , True ) -> []             -- remove trailing space
+      (False, _   , True ) -> t              -- remove trailing space
+      (False, True, False) -> t ++ ' ' : s   -- add space if none
+      _                    -> t ++ s
     where
-      t'          = showString t []
       (spc, rest) = span isSpace s
 
   closingOrPunctuation :: String -> Bool
@@ -121,10 +123,10 @@
 mkEsc :: Char -> Char -> ShowS
 mkEsc q = \case
   s | s == q -> showChar '\\' . showChar s
-  '\\'       -> showString "\\\\"
-  '\n'       -> showString "\\n"
-  '\t'       -> showString "\\t"
-  s          -> showChar s
+  '\\' -> showString "\\\\"
+  '\n' -> showString "\\n"
+  '\t' -> showString "\\t"
+  s -> showChar s
 
 prPrec :: Int -> Int -> Doc -> Doc
 prPrec i j = if j < i then parenth else id
@@ -152,8 +154,8 @@
     Language.Rzk.Syntax.Abs.VarIdent _ varidenttoken -> prPrec i 0 (concatD [prt 0 varidenttoken])
 
 instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where
@@ -179,7 +181,7 @@
     Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> prPrec i 0 (concatD [doc (showString "#define"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term1, doc (showString ":="), prt 0 term2])
 
 instance Print [Language.Rzk.Syntax.Abs.Command' a] where
-  prt _ []     = concatD []
+  prt _ [] = concatD []
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where
@@ -198,8 +200,8 @@
     Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
 
 instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.Param' a) where
@@ -210,8 +212,8 @@
     Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString "|"), prt 0 term2, doc (showString "}")])
 
 instance Print [Language.Rzk.Syntax.Abs.Param' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
@@ -228,8 +230,8 @@
     Language.Rzk.Syntax.Abs.ASCII_Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "|->"), prt 0 term2])
 
 instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.Term' a) where
@@ -289,6 +291,6 @@
     Language.Rzk.Syntax.Abs.ASCII_Second _ term -> prPrec i 6 (concatD [doc (showString "second"), prt 7 term])
 
 instance Print [Language.Rzk.Syntax.Abs.Term' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs
--- a/src/Language/Rzk/VSCode/Handlers.hs
+++ b/src/Language/Rzk/VSCode/Handlers.hs
@@ -8,10 +8,11 @@
 
 import           Control.Exception             (SomeException, evaluate, try)
 import           Control.Lens
-import           Control.Monad.Cont            (MonadIO (liftIO), forM_)
+import           Control.Monad                 (forM_, when)
+import           Control.Monad.IO.Class        (MonadIO (..))
 import           Data.Default.Class
 import           Data.List                     (sort, (\\))
-import           Data.Maybe                    (fromMaybe)
+import           Data.Maybe                    (fromMaybe, isNothing)
 import qualified Data.Text                     as T
 import qualified Data.Yaml                     as Yaml
 import           Language.LSP.Diagnostics      (partitionBySource)
@@ -32,7 +33,8 @@
 import           Language.Rzk.Syntax           (Module, VarIdent' (VarIdent),
                                                 parseModuleFile, printTree)
 import           Language.Rzk.VSCode.Env
-import           Language.Rzk.VSCode.State     (ProjectConfig (include))
+import           Language.Rzk.VSCode.Logging
+import           Rzk.Project.Config            (ProjectConfig (include))
 import           Rzk.TypeCheck
 
 -- | Given a list of file paths, reads them and parses them as Rzk modules,
@@ -66,18 +68,21 @@
 
 typecheckFromConfigFile :: LSP ()
 typecheckFromConfigFile = do
+  logInfo "Looking for rzk.yaml"
   root <- getRootPath
   case root of
     Nothing -> do
+      logWarning "Workspace has no root path, cannot find rzk.yaml"
       sendNotification SMethod_WindowShowMessage (ShowMessageParams MessageType_Warning "Cannot find the workspace root")
     Just rootPath -> do
       let rzkYamlPath = rootPath </> "rzk.yaml"
       eitherConfig <- liftIO $ Yaml.decodeFileEither @ProjectConfig rzkYamlPath
       case eitherConfig of
         Left err -> do
-          sendNotification SMethod_WindowShowMessage (ShowMessageParams MessageType_Warning (T.pack $ "Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err))
+          logError ("Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err)
 
         Right config -> do
+          logDebug "Starting typechecking"
           rawPaths <- liftIO $ globDir (map compile (include config)) rootPath
           let paths = concatMap sort rawPaths
 
@@ -85,6 +90,9 @@
           let cachedPaths = map fst cachedModules
               modifiedFiles = paths \\ cachedPaths
 
+          logDebug ("Found " ++ show (length cachedPaths) ++ " files in the cache")
+          logDebug (show (length modifiedFiles) ++ " files have been modified")
+
           (parseErrors, parsedModules) <- liftIO $ collectErrors <$> parseFiles modifiedFiles
           tcResults <- liftIO $ try $ evaluate $
             defaultTypeCheck (typecheckModulesWithLocationIncremental cachedModules parsedModules)
@@ -94,11 +102,14 @@
             Right (Left err) -> return ([err], [])    -- sort of impossible
             Right (Right (checkedModules, errors)) -> do
                 -- cache well-typed modules
+                logInfo (show (length checkedModules) ++ " modules successfully typechecked")
+                logInfo (show (length errors) ++ " errors found")
                 cacheTypecheckedModules checkedModules
                 return (errors, checkedModules)
 
           -- Reset all published diags
           -- TODO: remove this after properly grouping by path below, after which there can be an empty list of errors
+          -- TODO: handle clearing diagnostics for files that got removed from the project (rzk.yaml)
           forM_ paths $ \path -> do
             publishDiagnostics 0 (filePathToNormalizedUri path) Nothing (partitionBySource [])
 
@@ -161,9 +172,12 @@
 
 provideCompletions :: Handler LSP 'Method_TextDocumentCompletion
 provideCompletions req res = do
+  logInfo "Providing text completions"
   root <- getRootPath
+  when (isNothing root) $ logDebug "Not in a workspace. Cannot find root path for relative paths"
   let rootDir = fromMaybe "/" root
   cachedModules <- getCachedTypecheckedModules
+  logDebug ("Found " ++ show (length cachedModules) ++ " modules in the cache")
   let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri
   -- Take all the modules up to and including the currently open one
   let modules = takeWhileInc ((/= currentFile) . fst) cachedModules
@@ -174,6 +188,7 @@
             | otherwise = [x]
 
   let items = concatMap (declsToItems rootDir) modules
+  logDebug ("Sending " ++ show (length items) ++ " completion items")
   res $ Right $ InL items
   where
     declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]
diff --git a/src/Language/Rzk/VSCode/Logging.hs b/src/Language/Rzk/VSCode/Logging.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Rzk/VSCode/Logging.hs
@@ -0,0 +1,20 @@
+module Language.Rzk.VSCode.Logging where
+
+import           Colog.Core           (Severity (..), WithSeverity (..), (<&))
+import qualified Data.Text            as T
+import           Language.LSP.Logging (defaultClientLogger)
+import           Language.LSP.Server  (MonadLsp)
+
+
+logDebug :: MonadLsp c m => String -> m ()
+logDebug msg = defaultClientLogger <& T.pack msg `WithSeverity` Debug
+
+logInfo :: MonadLsp c m => String -> m ()
+logInfo msg = defaultClientLogger <& T.pack msg `WithSeverity` Info
+
+logWarning :: MonadLsp c m => String -> m ()
+logWarning msg = defaultClientLogger <& T.pack msg `WithSeverity` Warning
+
+-- | Error logs will also be shown to the user via `window/showMessage`
+logError :: MonadLsp c m => String -> m ()
+logError msg = defaultClientLogger <& T.pack msg `WithSeverity` Error
diff --git a/src/Language/Rzk/VSCode/Lsp.hs b/src/Language/Rzk/VSCode/Lsp.hs
--- a/src/Language/Rzk/VSCode/Lsp.hs
+++ b/src/Language/Rzk/VSCode/Lsp.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE OverloadedStrings     #-}
-{-# LANGUAGE TypeApplications      #-}
 
 module Language.Rzk.VSCode.Lsp where
 
@@ -20,6 +19,7 @@
 import           Language.Rzk.Syntax           (parseModuleSafe)
 import           Language.Rzk.VSCode.Env
 import           Language.Rzk.VSCode.Handlers
+import           Language.Rzk.VSCode.Logging
 import           Language.Rzk.VSCode.Tokenize  (tokenizeModule)
 
 -- | The maximum number of diagnostic messages to send to the client
@@ -39,12 +39,10 @@
     , notificationHandler SMethod_WorkspaceDidChangeWatchedFiles $ \msg -> do
         let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just
         if any ("rzk.yaml" `isSuffixOf`) modifiedPaths
-          then resetCacheForAllFiles
+          then do
+            logDebug "rzk.yaml modified. Clearing module cache"
+            resetCacheForAllFiles
           else resetCacheForFiles modifiedPaths
-        -- TODO: see what files changed and typecheck them again
-        --  Need to handle 3 events: added, changed, and deleted
-
-        -- Currently, this is only sent for changes in `rzk.yaml`, so it makes sense to typecheck again (unconditionally)
         typecheckFromConfigFile
     , notificationHandler SMethod_TextDocumentDidSave $ \_msg -> do
         -- TODO: check if the file is included in the config's `include` list.
@@ -67,9 +65,9 @@
               Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $
                 parseModuleSafe (T.unpack sourceCode)
         case possibleTokens of
-          Left _err -> do
+          Left err -> do
             -- Exception occurred when parsing the module
-            return ()
+            logWarning ("Failed to tokenize file: " ++ err)
           Right tokens -> do
             let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens
             case encoded of
@@ -95,10 +93,12 @@
   rzkEnv <- defaultRzkEnv
   runServer $
     ServerDefinition
-      { onConfigurationChange = const $ pure $ Right (),
-        doInitialize = const . pure . Right,
-        staticHandlers = const handlers,
-        interpretHandler = \env -> Iso (flip runReaderT rzkEnv . runLspT env) liftIO,
-        options = defaultOptions { optTextDocumentSync = Just syncOptions },
-        defaultConfig = ()
+      { configSection = "rzk"
+      , parseConfig = const . pure
+      , onConfigChange = const $ pure ()
+      , doInitialize = const . pure . Right
+      , staticHandlers = const handlers
+      , interpretHandler = \env -> Iso (flip runReaderT rzkEnv . runLspT env) liftIO
+      , options = defaultOptions { optTextDocumentSync = Just syncOptions }
+      , defaultConfig = ()
       }
diff --git a/src/Language/Rzk/VSCode/State.hs b/src/Language/Rzk/VSCode/State.hs
deleted file mode 100644
--- a/src/Language/Rzk/VSCode/State.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Language.Rzk.VSCode.State where
-
-import           Data.Yaml (FromJSON (..), (.!=), (.:), (.:?))
-import qualified Data.Yaml as Y
-
-data ProjectConfig = ProjectConfig
-  { include :: [FilePath]
-  , exclude :: [FilePath]
-  } deriving (Eq, Show)
-
-instance FromJSON ProjectConfig where
-  parseJSON (Y.Object v) =
-    ProjectConfig   <$>
-    v .:  "include" <*>
-    v .:? "exclude" .!= []
-  parseJSON _ = fail "Expected config value to be an object"
-
--- TODO: Add a "ServerState" data structure for holding the typechecking cache
diff --git a/src/Language/Rzk/VSCode/Tokenize.hs b/src/Language/Rzk/VSCode/Tokenize.hs
--- a/src/Language/Rzk/VSCode/Tokenize.hs
+++ b/src/Language/Rzk/VSCode/Tokenize.hs
@@ -6,7 +6,6 @@
                                               SemanticTokenModifiers (..),
                                               SemanticTokenTypes (..))
 import           Language.Rzk.Syntax
-import           Language.Rzk.Syntax.Print
 
 tokenizeModule :: Module -> [SemanticTokenAbsolute]
 tokenizeModule (Module _loc langDecl commands) = concat
diff --git a/src/Rzk/Main.hs b/src/Rzk/Main.hs
--- a/src/Rzk/Main.hs
+++ b/src/Rzk/Main.hs
@@ -3,21 +3,28 @@
 {-# LANGUAGE DeriveGeneric     #-}
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
+{-# LANGUAGE TypeApplications  #-}
 
 module Rzk.Main where
 
 import           Control.Monad           (forM, void)
 import           Data.List               (sort)
 import           Data.Version            (showVersion)
-#ifndef __GHCJS__
+
+#ifdef LSP
 import           Language.Rzk.VSCode.Lsp (runLsp)
 #endif
+
+import qualified Data.Yaml               as Yaml
 import           Options.Generic
+import           System.Directory        (doesPathExist)
 import           System.Exit             (exitFailure)
 import           System.FilePath.Glob    (glob)
 
 import qualified Language.Rzk.Syntax     as Rzk
 import           Paths_rzk               (version)
+import           Rzk.Project.Config
 import           Rzk.TypeCheck
 
 data Command
@@ -41,10 +48,10 @@
       Right _decls -> putStrLn "Everything is ok!"
 
   Lsp ->
-#ifndef __GHCJS__
+#ifdef LSP
     void runLsp
 #else
-    error "rzk lsp is not supported with a GHCJS build"
+    error "rzk lsp is not supported with this build"
 #endif
 
   Version -> putStrLn (showVersion version)
@@ -66,12 +73,29 @@
     []    -> error ("File(s) not found at " <> path)
     paths -> return (sort paths)
 
+extractFilesFromRzkYaml :: FilePath -> IO [FilePath]
+extractFilesFromRzkYaml rzkYamlPath = do
+  eitherConfig <- Yaml.decodeFileEither @ProjectConfig rzkYamlPath
+  case eitherConfig of
+    Left err -> do
+      error ("Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err)
+    Right ProjectConfig{..} -> do
+      return include
+
 parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Rzk.Module)]
 parseRzkFilesOrStdin = \case
   -- if no paths are given — read from stdin
   [] -> do
-    rzkModule <- parseStdin
-    return [("<stdin>", rzkModule)]
+    let rzkYamlPath = "rzk.yaml"
+    rzkYamlExists <- doesPathExist rzkYamlPath
+    if rzkYamlExists
+      then do
+        putStrLn ("Using Rzk project stucture specified in " <> rzkYamlPath)
+        paths <- extractFilesFromRzkYaml rzkYamlPath
+        parseRzkFilesOrStdin paths
+      else do
+        rzkModule <- parseStdin
+        return [("<stdin>", rzkModule)]
   -- otherwise — parse all given files in given order
   paths -> do
     expandedPaths <- foldMap globNonEmpty paths
@@ -87,7 +111,7 @@
 typecheckString :: String -> Either String String
 typecheckString moduleString = do
   rzkModule <- Rzk.parseModule moduleString
-  case defaultTypeCheck (typecheckModule Nothing rzkModule) of
+  case defaultTypeCheck (typecheckModules [rzkModule]) of
     Left err -> Left $ unlines
       [ "An error occurred when typechecking!"
       , "Rendering type error... (this may take a few seconds)"
diff --git a/src/Rzk/Project/Config.hs b/src/Rzk/Project/Config.hs
new file mode 100644
--- /dev/null
+++ b/src/Rzk/Project/Config.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Rzk.Project.Config where
+
+import           Data.Yaml (FromJSON (..), (.!=), (.:), (.:?))
+import qualified Data.Yaml as Y
+
+data ProjectConfig = ProjectConfig
+  { include :: [FilePath]
+  , exclude :: [FilePath]
+  } deriving (Eq, Show)
+
+instance FromJSON ProjectConfig where
+  parseJSON (Y.Object v) =
+    ProjectConfig   <$>
+    v .:  "include" <*>
+    v .:? "exclude" .!= []
+  parseJSON _ = fail "Expected config value to be an object"
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -10,6 +10,7 @@
 module Rzk.TypeCheck where
 
 import           Control.Applicative      ((<|>))
+import           Control.Monad            (forM, forM_, join, unless, when)
 import           Control.Monad.Except
 import           Control.Monad.Reader
 import           Data.Bifunctor           (first)
@@ -88,12 +89,12 @@
   [] -> return []
   m : ms -> do
     (decls, errs) <- typecheckModule Nothing m
-    if null errs
-      then
+    case errs of
+      err : _ -> do
+        throwError err
+      _ -> do
         localDeclsPrepared decls $
           (decls <>) <$> typecheckModules ms
-      else
-        return decls
 
 typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
 typecheckModuleWithLocation (path, module_) = do
@@ -1938,14 +1939,23 @@
                     switchVariance $  -- unifying in the negative position!
                       unifyTerms cube cube' -- FIXME: unifyCubes
                     enterScope orig' cube $ do
-                      case (mtope, mtope') of
-                        (Just tope, Just tope') -> do
-                          topeNF <- nfT tope
-                          topeNF' <- nfT tope'
-                          unifyTopes topeNF topeNF'
-                        (Nothing, Nothing)      -> return ()
-                        (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
-                        (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
+                      case ret' of
+                        -- UniverseTopeT{} ->
+                        --   (Just tope, Just tope') -> do
+                        --     topeNF <- nfT tope
+                        --     topeNF' <- nfT tope'
+                        --     unifyTopes topeNF topeNF'
+                        --   (Nothing, Nothing)      -> return ()
+                        --   (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
+                        --   (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
+                        _ -> case (mtope, mtope') of
+                          (Just tope, Just tope') -> do
+                            topeNF <- nfT tope
+                            topeNF' <- nfT tope'
+                            unifyTopes topeNF topeNF'
+                          (Nothing, Nothing)      -> return ()
+                          (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
+                          (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
                       case mterm of
                         Nothing -> unifyTerms ret ret'
                         Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'