diff --git a/dune-project b/dune-project
index 7e80710..c6a93db 100644
--- a/dune-project
+++ b/dune-project
@@ -7,9 +7,9 @@
 (source
  (github username/reponame))
 
-(authors "Author Name")
+(authors "William Ball")
 
-(maintainers "Maintainer Name")
+(maintainers "William Ball")
 
 (license LICENSE)
 
@@ -19,7 +19,7 @@
  (name proof_checker)
  (synopsis "A short synopsis")
  (description "A longer description")
- (depends ocaml dune)
+ (depends ocaml dune fmlib_parse sedlex)
  (tags
   (topics "to describe" your project)))
 
diff --git a/lib/dune b/lib/dune
index f3c2831..75cf0a4 100644
--- a/lib/dune
+++ b/lib/dune
@@ -1,2 +1,3 @@
 (library
- (name proof_checker))
+ (name proof_checker)
+ (libraries kernel pfparser))
diff --git a/lib/kernel/dune b/lib/kernel/dune
new file mode 100644
index 0000000..05e5dc2
--- /dev/null
+++ b/lib/kernel/dune
@@ -0,0 +1,2 @@
+(library
+ (name kernel))
diff --git a/lib/formula.ml b/lib/kernel/formula.ml
similarity index 95%
rename from lib/formula.ml
rename to lib/kernel/formula.ml
index 43730c3..a3a7409 100644
--- a/lib/formula.ml
+++ b/lib/kernel/formula.ml
@@ -85,11 +85,11 @@ let to_string formula =
       match formula with
       | Relation (r, terms) ->
           sprintf "%s(%s)" r
-            (String.concat ", " (List.map (Term.to_string ~binders) terms))
+            (String.concat ", " (List.map (Term.to_string binders) terms))
       | Equal (t1, t2) ->
           sprintf "%s = %s"
-            (Term.to_string ~binders t1)
-            (Term.to_string ~binders t2)
+            (Term.to_string binders t1)
+            (Term.to_string binders t2)
       | Bottom -> "⊥"
       | Neg f -> sprintf "¬%s" (aux depth binders Negation f)
       | Conj (f1, f2) -> sprintf "%s ∧ %s" (step f1) (step f2)
diff --git a/lib/formula.mli b/lib/kernel/formula.mli
similarity index 66%
rename from lib/formula.mli
rename to lib/kernel/formula.mli
index a14047e..b18182a 100644
--- a/lib/formula.mli
+++ b/lib/kernel/formula.mli
@@ -10,6 +10,16 @@ type t =
   | Forall of t
   | Exists of t
 
+type precedence =
+  | Atomic
+  | Negation
+  | Conjunction
+  | Disjunction
+  | Implication
+  | Biconditional
+  | Quantifier
+
+val precedence_of : t -> precedence
 val match_term : Term.t -> t -> t -> Term.match_result
 val occurs : Term.t -> t -> bool
 val to_string : t -> string
diff --git a/lib/proof.ml b/lib/kernel/proof.ml
similarity index 100%
rename from lib/proof.ml
rename to lib/kernel/proof.ml
diff --git a/lib/proof.mli b/lib/kernel/proof.mli
similarity index 100%
rename from lib/proof.mli
rename to lib/kernel/proof.mli
diff --git a/lib/term.ml b/lib/kernel/term.ml
similarity index 91%
rename from lib/term.ml
rename to lib/kernel/term.ml
index 175157f..f725b7c 100644
--- a/lib/term.ml
+++ b/lib/kernel/term.ml
@@ -41,12 +41,10 @@ let rec occurs t = function
   | Function (_, ts) -> List.exists (occurs t) ts
   | s -> t = s
 
-exception UnboundVariable
-
-let to_string ~binders =
+let to_string binders =
   let open Format in
   let rec aux = function
-    | Var v -> ( try List.nth binders v with _ -> raise UnboundVariable)
+    | Var v -> List.nth binders v
     | Const c -> c
     | Free f -> f
     | Function (f, args) ->
diff --git a/lib/term.mli b/lib/kernel/term.mli
similarity index 80%
rename from lib/term.mli
rename to lib/kernel/term.mli
index 72701da..7a0d0d5 100644
--- a/lib/term.mli
+++ b/lib/kernel/term.mli
@@ -12,7 +12,4 @@ val merge_result : match_result -> match_result -> match_result
 val match_term : t -> t -> t -> match_result
 val inc_var : t -> t
 val occurs : t -> t -> bool
-
-exception UnboundVariable
-
-val to_string : binders:string list -> t -> string
+val to_string : string list -> t -> string
diff --git a/lib/parser/dune b/lib/parser/dune
new file mode 100644
index 0000000..05b635d
--- /dev/null
+++ b/lib/parser/dune
@@ -0,0 +1,3 @@
+(library
+ (name pfparser)
+ (libraries kernel sedlex fmlib_parse))
diff --git a/lib/parser/parser.ml b/lib/parser/parser.ml
new file mode 100644
index 0000000..179d429
--- /dev/null
+++ b/lib/parser/parser.ml
@@ -0,0 +1 @@
+let x = 3
diff --git a/proof_checker.opam b/proof_checker.opam
index b296c11..49ad67c 100644
--- a/proof_checker.opam
+++ b/proof_checker.opam
@@ -2,8 +2,8 @@
 opam-version: "2.0"
 synopsis: "A short synopsis"
 description: "A longer description"
-maintainer: ["Maintainer Name"]
-authors: ["Author Name"]
+maintainer: ["William Ball"]
+authors: ["William Ball"]
 license: "LICENSE"
 tags: ["topics" "to describe" "your" "project"]
 homepage: "https://github.com/username/reponame"
@@ -12,6 +12,8 @@ bug-reports: "https://github.com/username/reponame/issues"
 depends: [
   "ocaml"
   "dune" {>= "3.16"}
+  "fmlib_parse"
+  "sedlex"
   "odoc" {with-doc}
 ]
 build: [