diff --git a/.hlint.yaml b/.hlint.yaml
deleted file mode 100644
index df9b14e18a..0000000000
--- a/.hlint.yaml
+++ /dev/null
@@ -1,89 +0,0 @@
-# Based on HLint configuration file from https://github.com/ndmitchell/hlint
-
-- arguments: [--color]
-
-# ------------------------------------------------------------------------------
-# RESTRICTIONS
-# ------------------------------------------------------------------------------
-
-- extensions:
- - default: false
- - name:
- - ApplicativeDo
- - DataKinds
- - DerivingStrategies
- - GADTs
- - ImportQualifiedPost
- - LambdaCase
- - NoImplicitPrelude
- - OverloadedStrings
- - QuantifiedConstraints
- - QuasiQuotes
- - RecordWildCards
- - StandaloneKindSignatures
- - TemplateHaskell
- - TypeFamilyDependencies
- - UndecidableInstances
- - UnicodeSyntax
- - GeneralizedNewtypeDeriving
-
-- flags:
- - default: false
- - name:
- - -Wall
- - -Wcompat
- - -Wderiving-defaults
- - -Widentities
- - -Wincomplete-patterns
- - -Wincomplete-record-updates
- - -Wincomplete-uni-patterns
- - -Wmissing-deriving-strategies
- - -Wredundant-constraints
- - -O2 -flate-specialise -fspecialise-aggressively
-
-- modules:
- # if you import Data.Set qualified, it must be as 'Set'
- - { name: [Data.Set, Data.HashSet], as: Set }
- - { name: [Data.Map, Data.HashMap.Strict, Data.HashMap.Lazy], as: Map }
- # - {name: Control.Arrow, within: []} # Certain modules are banned entirely
-
-- functions:
- - { name: Data.List.NonEmpty.nub, within: [] }
- - { name: Data.List.NonEmpty.nubBy, within: [] }
-
-# ------------------------------------------------------------------------------
-# OTHER HINTS
-# ------------------------------------------------------------------------------
-
-# - warn: {name: Use explicit module export list}
-
-# ------------------------------------------------------------------------------
-# HINTS
-# ------------------------------------------------------------------------------
-
-- error: { lhs: idea Warning, rhs: warn }
-- error: { lhs: idea Suggestion, rhs: suggest }
-- error: { lhs: ideaN Warning, rhs: warnN }
-- error: { lhs: ideaN Suggestion, rhs: suggestN }
-
-- error: { lhs: occNameString (occName (unLoc x)), rhs: rdrNameStr x }
-- error: { lhs: occNameString (occName x), rhs: occNameStr x }
-- error:
- {
- lhs: noLoc (HsVar noExtField (noLoc (mkRdrUnqual (mkVarOcc x)))),
- rhs: strToVar x,
- }
-
-# ------------------------------------------------------------------------------
-# IGNORES
-# ------------------------------------------------------------------------------
-
-- ignore: { name: Use let, within: [Test.All] }
-- ignore: { name: Use String }
-- ignore: { name: Avoid restricted qualification }
-- ignore: { name: Redundant multi-way if }
-- ignore: { name: Redundant bracket }
-- ignore: { name: Eta reduce }
-- ignore: { name: Avoid restricted alias }
-- ignore: { name: Use tuple-section }
-- ignore: { name: Use map with tuple-section }
diff --git a/Makefile b/Makefile
index c80ba82944..040b74f68a 100644
--- a/Makefile
+++ b/Makefile
@@ -42,7 +42,6 @@ all: build
clean: clean-runtime
@${STACK} clean --full
@rm -rf .hie
- @rm -rf book
.PHONY: clean-hard
clean-hard: clean
@@ -158,16 +157,6 @@ check-ormolu: export ORMOLUMODE = check
check-ormolu:
@${MAKE} ormolu
-HLINT?=stack exec -- hlint
-HLINTFLAGS?=
-HLINTQUIET :=
-
-.PHONY : hlint
-hlint :
- ${HLINT} ${HLINTFLAGS} app ${HLINTQUIET}
- ${HLINT} ${HLINTFLAGS} src ${HLINTQUIET}
- ${HLINT} ${HLINTFLAGS} test ${HLINTQUIET}
-
PRECOMMIT := $(shell command -v pre-commit 2> /dev/null)
.PHONY : install-pre-commit
diff --git a/assets/images/tara-magicien.png b/assets/images/tara-magicien.png
deleted file mode 100644
index 9547cd3aae..0000000000
Binary files a/assets/images/tara-magicien.png and /dev/null differ
diff --git a/assets/images/tara-seating.svg b/assets/images/tara-seating.svg
deleted file mode 100644
index 14d49623f6..0000000000
--- a/assets/images/tara-seating.svg
+++ /dev/null
@@ -1 +0,0 @@
-
\ No newline at end of file
diff --git a/assets/images/tara-smiling.png b/assets/images/tara-smiling.png
deleted file mode 100644
index a37360a1d4..0000000000
Binary files a/assets/images/tara-smiling.png and /dev/null differ
diff --git a/assets/images/tara-teaching.png b/assets/images/tara-teaching.png
deleted file mode 100644
index 0a14b307c0..0000000000
Binary files a/assets/images/tara-teaching.png and /dev/null differ
diff --git a/assets/images/tara-teaching.svg b/assets/images/tara-teaching.svg
deleted file mode 100644
index 98ca5d366a..0000000000
--- a/assets/images/tara-teaching.svg
+++ /dev/null
@@ -1 +0,0 @@
-
diff --git a/book.toml b/book.toml
deleted file mode 100644
index 2317722f2d..0000000000
--- a/book.toml
+++ /dev/null
@@ -1,60 +0,0 @@
-[book]
-title = "The Juvix Book"
-authors = [ "Jonathan Prieto-Cubides" , "Jan Mas Rovira" , "Paul Cadman" , "Lukasz Czajka" ]
-language = "en"
-multilingual = false
-src = "docs"
-
-[build]
-create-missing = true
-
-[preprocessor.index]
-
-[preprocessor.links]
-
-[preprocessor.pagetoc]
-
-[preprocessor.katex]
-renderers = ["html"]
-static-css = false
-include-src = false
-block-delimiter = {left = "$$", right = "$$"}
-inline-delimiter = {left = "$", right = "$"}
-macros = "theme/latex-macros.txt"
-
-[output.katex]
-
-[output.html]
-default-theme = "light"
-preferred-dark-theme = "Ayu"
-copy-fonts = true
-additional-css = ["theme/pagetoc.css", "theme/juvix.css"]
-additional-js = ["theme/pagetoc.js", "theme/juvix.js", "theme/pascal.js"]
-no-section-label = false
-git-repository-url = "https://github.com/anoma/juvix"
-git-repository-icon = "fa-github"
-
-[output.html.fold]
-enable = true # whether or not to enable section folding
-level = 0 # the depth to start folding
-
-[output.html.search]
-enable = true # enables the search feature
-limit-results = 15 # maximum number of search results
-teaser-word-count = 30 # number of words used for a search result teaser
-use-boolean-and = true # multiple search terms must all match
-boost-title = 2 # ranking boost factor for matches in headers
-boost-hierarchy = 1 # ranking boost factor for matches in page names
-boost-paragraph = 1 # ranking boost factor for matches in text
-expand = true # partial words will match longer terms
-heading-split-level = 2 # link results to heading levels
-copy-js = true # include Javascript code for search
-
-[output.linkcheck]
-follow-web-links = false
-traverse-parent-directories = false
-exclude = [ ]
-user-agent = "mdbook-linkcheck-0.4.0"
-cache-timeout = 43200
-[output.linkcheck.http-headers]
-'crates\.io' = ["Accept: text/html"]
diff --git a/licenses/agda/LICENSE b/licenses/agda/LICENSE
deleted file mode 100644
index af3fef33e8..0000000000
--- a/licenses/agda/LICENSE
+++ /dev/null
@@ -1,101 +0,0 @@
-Copyright (c) 2005-2021 remains with the authors.
-Agda 2 was originally written by Ulf Norell,
-partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama,
-and from Agdalight by Ulf Norell and Andreas Abel.
-
-Agda 2 is currently actively developed mainly by Andreas Abel,
-Guillaume Allais, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Nils
-Anders Danielsson, Ulf Norell, Andrés Sicard-Ramírez, and Andrea
-Vezzosi.
-
-Further, Agda 2 has received contributions by, amongst others, Stevan
-Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie,
-James Chapman, Dominique Devriese, Péter Diviánszky, Robert Estelle,
-Olle Fredriksson, Adam Gundry, Daniel Gustafsson, Philipp Hausmann,
-Alan Jeffrey, Wolfram Kahl, Wen Kokke, John Leo, Fredrik Lindblad,
-Víctor López Juan, Ting-Gan Lua, Francesco Mazzoli, Stefan Monnier,
-Guilhem Moulin, Fredrik Nordvall Forsberg, Nicolas Pouillard, Jonathan
-Prieto, Christian Sattler, Makoto Takeyama, Noam Zeilberger, and Tesla
-Ice Zhang. The full list of contributors is available at
-https://github.com/agda/agda/graphs/contributors or from the git
-repository via ``git shortlog -sne``.
-
-Permission is hereby granted, free of charge, to any person obtaining
-a copy of this software and associated documentation files (the
-"Software"), to deal in the Software without restriction, including
-without limitation the rights to use, copy, modify, merge, publish,
-distribute, sublicense, and/or sell copies of the Software, and to
-permit persons to whom the Software is furnished to do so, subject to
-the following conditions:
-
-The above copyright notice and this permission notice shall be
-included in all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
-IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
-CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
-TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
-SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-
---------------------------------------------------------------------------------
-
-The file src/full/Agda/Utils/Maybe/Strict.hs (and the following
-license text?) uses the following license:
-
-Copyright (c) Roman Leshchinskiy 2006-2007
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions
-are met:
-
-1. Redistributions of source code must retain the above copyright
- notice, this list of conditions and the following disclaimer.
-2. Redistributions in binary form must reproduce the above copyright
- notice, this list of conditions and the following disclaimer in the
- documentation and/or other materials provided with the distribution.
-3. Neither the name of the author nor the names of his contributors
- may be used to endorse or promote products derived from this software
- without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE CONTRIBUTORS ``AS IS'' AND
-ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
-ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE
-FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
-DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
-OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
-HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
-LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
-OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
-SUCH DAMAGE.
-
-------------------------------------------------------------------------
-
-The file src/data/html/highlight-hover.js (and the following licence
-text?) seems to use the following licence:
-
-Copyright 2002-2010, Simon Marlow. All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-- Redistributions of source code must retain the above copyright notice,
-this list of conditions and the following disclaimer.
-
-- Redistributions in binary form must reproduce the above copyright notice,
-this list of conditions and the following disclaimer in the documentation
-and/or other materials provided with the distribution.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS "AS IS" AND ANY
-EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
-PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
-LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
-CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
-SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
-BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
-WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
-OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
-IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/licenses/agda/readme.org b/licenses/agda/readme.org
deleted file mode 100644
index a55a2abe90..0000000000
--- a/licenses/agda/readme.org
+++ /dev/null
@@ -1,3 +0,0 @@
-#+title: Readme
-
-We have copied [[https://github.com/agda/agda][Agda]]'s input method and adapted it to Juvix.
diff --git a/theme/index.hbs b/theme/index.hbs
deleted file mode 100644
index 89e1e09fc8..0000000000
--- a/theme/index.hbs
+++ /dev/null
@@ -1,323 +0,0 @@
-
-
-