diff --git a/package.json b/package.json
index ae56105..bcd82c8 100644
--- a/package.json
+++ b/package.json
@@ -10,7 +10,8 @@
     "preview": "vite preview",
     "res:build": "rescript",
     "res:clean": "rescript clean",
-    "res:dev": "rescript -w"
+    "res:dev": "rescript -w",
+    "res:format": "rescript format -all"
   },
   "dependencies": {
     "@rescript/react": "^0.13.1",
diff --git a/src/AxiomSet.res b/src/AxiomSet.res
index f4f8410..d52933d 100644
--- a/src/AxiomSet.res
+++ b/src/AxiomSet.res
@@ -1,68 +1,83 @@
 open Signatures
 open Component
 module Make = (
-  Term : TERM, 
-  Judgment : JUDGMENT with module Term := Term,
-  JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment) => {
-  module Rule = Rule.Make(Term,Judgment)
-  module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
-  module Ports = Ports(Term,Judgment)
-  type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t,~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
-  
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
+) => {
+  module Rule = Rule.Make(Term, Judgment)
+  module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
+  module Ports = Ports(Term, Judgment)
+  type props = {
+    content: string,
+    imports: Ports.t,
+    onLoad: (~exports: Ports.t, ~string: string=?) => unit,
+    onChange: (string, ~exports: Ports.t) => unit,
+  }
+
   let deserialise = (str: string) => {
     let cur = ref(str)
     let go = ref(true)
-    let results = Dict.make()    
+    let results = Dict.make()
     let ret = ref(Error("impossible"))
     while go.contents {
-      switch Rule.parseTopLevel(cur.contents,~scope=[]) {
-      | Ok((t,n),rest) => {
-          if n->String.trim == "" {
+      switch Rule.parseTopLevel(cur.contents, ~scope=[]) {
+      | Ok((t, n), rest) => if n->String.trim == "" {
+          go := false
+          ret := Error("Rule given with no name")
+        } else {
+          Dict.set(results, n, t)
+          if rest->String.trim == "" {
             go := false
-            ret := Error("Rule given with no name")
-          } else { 
-            Dict.set(results,n,t)
-            if rest->String.trim == "" {
-              go := false
-              ret := Ok(results)
-            } else {
-              cur := rest
-            }
+            ret := Ok(results)
+          } else {
+            cur := rest
           }
         }
-      | Error(e) => { go := false; ret := Error(e) }
+      | Error(e) => {
+          go := false
+          ret := Error(e)
+        }
       }
     }
     ret.contents
   }
-  
-  let make = (props ) => {
+
+  let make = props => {
     switch deserialise(props.content) {
     | Ok(s) => {
         React.useEffect(() => {
-          // Run effects          
-          props.onLoad(~exports= {Ports.facts: s, ruleStyle: None});
+          // Run effects
+          props.onLoad(~exports={Ports.facts: s, ruleStyle: None})
           None // or Some(() => {})
         }, [])
-        
-        <div className={"axiom-set axiom-set-"->String.concat(String.make(props.imports.ruleStyle->Option.getOr(Hybrid)))}>
-        { Dict.toArray(s)->Array.mapWithIndex(((n,r), i) => 
-          <RuleView rule={r} scope={[]} key={String.make(i)} style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
-            {React.string(n)}
-            //<Name content={n} onChange={(_) => Error("BLAH!")} />
-          </RuleView>)
-          ->React.array
-        }
+
+        <div
+          className={"axiom-set axiom-set-"->String.concat(
+            String.make(props.imports.ruleStyle->Option.getOr(Hybrid)),
+          )}>
+          {Dict.toArray(s)
+          ->Array.mapWithIndex(((n, r), i) =>
+            <RuleView
+              rule={r}
+              scope={[]}
+              key={String.make(i)}
+              style={props.imports.ruleStyle->Option.getOr(Hybrid)}>
+              {React.string(n)}
+              //<Name content={n} onChange={(_) => Error("BLAH!")} />
+            </RuleView>
+          )
+          ->React.array}
         </div>
       }
     | Error(e) => {
-    React.useEffect(() => {
-      // Run effects
-      props.onLoad(~exports= {Ports.facts: Dict.make(), ruleStyle: None});
-        None // or Some(() => {})
-      }, [])
-      <div className="error"> {React.string(e)} </div>
+        React.useEffect(() => {
+          // Run effects
+          props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None})
+          None // or Some(() => {})
+        }, [])
+        <div className="error"> {React.string(e)} </div>
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/Component.res b/src/Component.res
index 56dd6cf..a847d75 100644
--- a/src/Component.res
+++ b/src/Component.res
@@ -1,21 +1,26 @@
 open Signatures
 module type PORTS = {
   type t
-  let combine : (t,t) => t
+  let combine: (t, t) => t
   let empty: t
 }
-module Ports = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
+module Ports = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
   module Rule = Rule.Make(Term, Judgment)
-  type t = { facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style>  }
-  let empty = { facts: Dict.make(), ruleStyle: None }
-  let combine = (p1,p2) => {
-    let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts);
-    let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x));
-    { facts, ruleStyle }
+  type t = {facts: Dict.t<Rule.t>, ruleStyle: option<RuleView.style>}
+  let empty = {facts: Dict.make(), ruleStyle: None}
+  let combine = (p1, p2) => {
+    let facts = Dict.copy(p1.facts)->Dict.assign(p2.facts)
+    let ruleStyle = p2.ruleStyle->Option.mapOr(p1.ruleStyle, x => Some(x))
+    {facts, ruleStyle}
   }
 }
 module type COMPONENT = {
-  module Ports : PORTS
-  type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t, ~string:string=?) => (),onChange: (string,~exports:Ports.t) => ()  }
-  let make :  props => React.element
+  module Ports: PORTS
+  type props = {
+    content: string,
+    imports: Ports.t,
+    onLoad: (~exports: Ports.t, ~string: string=?) => unit,
+    onChange: (string, ~exports: Ports.t) => unit,
+  }
+  let make: props => React.element
 }
diff --git a/src/ConfigBlock.res b/src/ConfigBlock.res
index 2e2b0f4..6be9d6b 100644
--- a/src/ConfigBlock.res
+++ b/src/ConfigBlock.res
@@ -1,37 +1,48 @@
 open Signatures
 open Component
 
-module Make = (
-  Term : TERM, 
-  Judgment : JUDGMENT with module Term := Term
-) => {
-  module Ports = Ports(Term,Judgment)
+module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
+  module Ports = Ports(Term, Judgment)
   open RuleView
-  type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t) => (), onChange: (string,~exports:Ports.t) => () }
-  let deserialise = (str) => switch str {
-  | "Gentzen" => Gentzen
-  | "Linear" => Linear
-  | "Hybrid" => Hybrid
-  | _ => Hybrid
+  type props = {
+    content: string,
+    imports: Ports.t,
+    onLoad: (~exports: Ports.t) => unit,
+    onChange: (string, ~exports: Ports.t) => unit,
   }
-  let make = (props) => {
-    let (style,setStyle) = React.useState (_=>deserialise(props.content))
+  let deserialise = str =>
+    switch str {
+    | "Gentzen" => Gentzen
+    | "Linear" => Linear
+    | "Hybrid" => Hybrid
+    | _ => Hybrid
+    }
+  let make = props => {
+    let (style, setStyle) = React.useState(_ => deserialise(props.content))
     React.useEffect(() => {
-      props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle:Some(style)})  
+      props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: Some(style)})
       None
-    },[])
-    let onChange= (e) => {
+    }, [])
+    let onChange = e => {
       let target = JsxEvent.Form.target(e)
       let value: string = target["value"]
       let sty = deserialise(value)
       setStyle(_ => sty)
-      
-      props.onChange(value,~exports={Ports.facts: Dict.make(), ruleStyle:Some(sty)})
+
+      props.onChange(value, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
     }
-    [Gentzen,Linear,Hybrid]->Array.map(n =>
-      <input type_="radio" id={"style_"->String.concat(String.make(n))} key={String.make(n)}  name="style" onChange value={String.make(n)} checked={style==n}/>
-    )->React.array
-    
+    [Gentzen, Linear, Hybrid]
+    ->Array.map(n =>
+      <input
+        type_="radio"
+        id={"style_"->String.concat(String.make(n))}
+        key={String.make(n)}
+        name="style"
+        onChange
+        value={String.make(n)}
+        checked={style == n}
+      />
+    )
+    ->React.array
   }
 }
-
diff --git a/src/Editable.res b/src/Editable.res
index a6f304a..82c6afd 100644
--- a/src/Editable.res
+++ b/src/Editable.res
@@ -1,44 +1,53 @@
 open Component
 
-module TextArea = (Underlying : COMPONENT) => {
+module TextArea = (Underlying: COMPONENT) => {
   module Ports = Underlying.Ports
-  type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t, ~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
-  let make = (props) => {
-    let (editing,setEditing) = React.useState (_ => false)
-    let (text,setText) = React.useState (_ => props.content)
-    let onTextChange= (ev: JsxEvent.Form.t) => {
+  type props = {
+    content: string,
+    imports: Ports.t,
+    onLoad: (~exports: Ports.t, ~string: string=?) => unit,
+    onChange: (string, ~exports: Ports.t) => unit,
+  }
+  let make = props => {
+    let (editing, setEditing) = React.useState(_ => false)
+    let (text, setText) = React.useState(_ => props.content)
+    let onTextChange = (ev: JsxEvent.Form.t) => {
       let target = JsxEvent.Form.target(ev)
       let value: string = target["value"]
       setText(_ => value)
     }
-    let done = (_) => {
-      setEditing(_=>false)
+    let done = _ => {
+      setEditing(_ => false)
     }
     if editing {
       <div>
         <textarea className="editor-textArea" value={text} onChange={onTextChange} />
         <div className="editor-controls">
-        <span className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}>
-        </span>
+          <span
+            className="editor-button button-icon button-icon-blue typcn typcn-tick" onClick={done}
+          />
         </div>
       </div>
     } else {
       <div>
-      <Underlying
-        content={text}
-        imports={props.imports}
-        onLoad={(~exports,~string=?) => {
-          props.onLoad(~exports,~string=string->Option.getOr(text))
-        }}
-        onChange={(string, ~exports) => {
-          setText(_=>string)
-          props.onChange(string,~exports)
-        }} />
-      <div className="editor-controls">
-      <span className="editor-button button-icon button-icon-blue typcn typcn-edit" onClick={_ => setEditing(_ => true)}>
-      </span>
-      </div>
+        <Underlying
+          content={text}
+          imports={props.imports}
+          onLoad={(~exports, ~string=?) => {
+            props.onLoad(~exports, ~string=string->Option.getOr(text))
+          }}
+          onChange={(string, ~exports) => {
+            setText(_ => string)
+            props.onChange(string, ~exports)
+          }}
+        />
+        <div className="editor-controls">
+          <span
+            className="editor-button button-icon button-icon-blue typcn typcn-edit"
+            onClick={_ => setEditing(_ => true)}
+          />
+        </div>
       </div>
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/Method.res b/src/Method.res
index 718be22..2e39750 100644
--- a/src/Method.res
+++ b/src/Method.res
@@ -1,96 +1,112 @@
 open Signatures
 open Util
-module Context = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
-  module Rule = Rule.Make(Term,Judgment)
+module Context = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
+  module Rule = Rule.Make(Term, Judgment)
   type rec t = {
-    fixes: array<Term.meta>, 
+    fixes: array<Term.meta>,
     facts: Dict.t<Rule.t>,
   }
 }
 
 module type PROOF_METHOD = {
-  module Term : TERM
-  module Judgment : JUDGMENT with module Term := Term
-  module Rule : module type of Rule.Make(Term,Judgment)
-  module Context : module type of Context(Term,Judgment)
+  module Term: TERM
+  module Judgment: JUDGMENT with module Term := Term
+  module Rule: module type of Rule.Make(Term, Judgment)
+  module Context: module type of Context(Term, Judgment)
   type t<'a>
-  let keywords : array<string>
-  let check : (t<'a>, Context.t, Judgment.t, 
-    ('a, Rule.t) => 'b) => result<t<'b>,string>
-  let uncheck : (t<'a>, 'a => 'b) => t<'b>
-  let parse : (string, ~keyword: string, ~scope: array<Term.meta>,~gen: Term.gen,
-              ~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen) 
-                          => result<('a,string),string> )
-          => result<(t<'a>,string),string>
-  let prettyPrint : (t<'a>,~scope: array<Term.meta>,~indentation:int=?,
-                    ~subprinter: ('a,~scope:array<Term.meta>,~indentation:int=?)
-                    =>string) 
-          => string
+  let keywords: array<string>
+  let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string>
+  let uncheck: (t<'a>, 'a => 'b) => t<'b>
+  let parse: (
+    string,
+    ~keyword: string,
+    ~scope: array<Term.meta>,
+    ~gen: Term.gen,
+    ~subparser: (string, ~scope: array<Term.meta>, ~gen: Term.gen) => result<('a, string), string>,
+  ) => result<(t<'a>, string), string>
+  let prettyPrint: (
+    t<'a>,
+    ~scope: array<Term.meta>,
+    ~indentation: int=?,
+    ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
+  ) => string
 }
 
-
-module Derivation = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term
-) => {  
-  module Rule = Rule.Make(Term,Judgment)
-  module Context = Context(Term,Judgment)
+module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
+  module Rule = Rule.Make(Term, Judgment)
+  module Context = Context(Term, Judgment)
   type t<'a> = {
     ruleName: string,
     instantiation: array<Term.t>,
-    subgoals: array<'a>
+    subgoals: array<'a>,
   }
-  let uncheck = (it : t<'a>, f) => {
-    { ruleName: it.ruleName, 
-      instantiation: it.instantiation, 
-      subgoals: it.subgoals->Array.map(f)
+  let uncheck = (it: t<'a>, f) => {
+    {
+      ruleName: it.ruleName,
+      instantiation: it.instantiation,
+      subgoals: it.subgoals->Array.map(f),
     }
   }
   exception InternalParseError(string)
   let keywords = ["by"]
-  let prettyPrint = (it : t<'a>, ~scope,~indentation=0,
-    ~subprinter: ('a,~scope:array<Term.meta>, ~indentation:int=?)=>string) => {
-    let args = it.instantiation->Array.map(t => Term.prettyPrint(t,~scope));
+  let prettyPrint = (
+    it: t<'a>,
+    ~scope,
+    ~indentation=0,
+    ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
+  ) => {
+    let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope))
     "by ("
-      ->String.concat(Array.join([it.ruleName,...args]," "))
-      ->String.concat(") {")
-      ->String.concat(if Array.length(it.subgoals) > 0 { newline } else { "" })
-      ->String.concat(it.subgoals
-          ->Array.map(s => subprinter(s, ~scope,~indentation=indentation+2))
-          ->Array.join(newline))
-      ->String.concat("}")
+    ->String.concat(Array.join([it.ruleName, ...args], " "))
+    ->String.concat(") {")
+    ->String.concat(
+      if Array.length(it.subgoals) > 0 {
+        newline
+      } else {
+        ""
+      },
+    )
+    ->String.concat(
+      it.subgoals
+      ->Array.map(s => subprinter(s, ~scope, ~indentation=indentation + 2))
+      ->Array.join(newline),
+    )
+    ->String.concat("}")
   }
   let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
     let cur = ref(String.trim(input))
-    if (cur.contents->String.get(0) == Some("(")) {
-      switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {      
-      | Ok((ruleName,rest)) => {
+    if cur.contents->String.get(0) == Some("(") {
+      switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {
+      | Ok((ruleName, rest)) => {
           cur := rest
-          let instantiation = [];
+          let instantiation = []
           let it = ref(Error(""))
-          while {it := Term.parse(cur.contents,~scope,~gen);
-                 it.contents->Result.isOk} {
-            let (val, rest) = it.contents->Result.getExn     
+          while {
+            it := Term.parse(cur.contents, ~scope, ~gen)
+            it.contents->Result.isOk
+          } {
+            let (val, rest) = it.contents->Result.getExn
             Array.push(instantiation, val)
             cur := String.trim(rest)
           }
-          if (cur.contents->String.get(0) == Some(")")) {
+          if cur.contents->String.get(0) == Some(")") {
             cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
             let subgoals = []
-            if (cur.contents->String.get(0) == Some("{")) {
+            if cur.contents->String.get(0) == Some("{") {
               cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
               try {
-                while (cur.contents->String.get(0) != Some("}")) {
-                  switch subparser(cur.contents,~scope,~gen) {
+                while cur.contents->String.get(0) != Some("}") {
+                  switch subparser(cur.contents, ~scope, ~gen) {
                   | Ok((sg, rest)) => {
-                      Array.push(subgoals,sg)
+                      Array.push(subgoals, sg)
                       cur := String.trim(rest)
                     }
                   | Error(e) => raise(InternalParseError(e))
                   }
-                } 
-                if (cur.contents->String.get(0) == Some("}")) {
+                }
+                if cur.contents->String.get(0) == Some("}") {
                   cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
-                  Ok(({ruleName,instantiation,subgoals},cur.contents))
+                  Ok(({ruleName, instantiation, subgoals}, cur.contents))
                 } else {
                   Error("} or subgoal proof expected")
                 }
@@ -98,7 +114,7 @@ module Derivation = (
               | InternalParseError(e) => Error(e)
               }
             } else {
-              Error("{ expected")  
+              Error("{ expected")
             }
           } else {
             Error(") or term expected")
@@ -110,110 +126,123 @@ module Derivation = (
       Error("Expected (")
     }
   }
-  let check = (it: t<'a>, ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
+  let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
     switch ctx.facts->Dict.get(it.ruleName) {
-    | None => 
-      Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'") )
+    | None => Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'"))
     | Some(rule) if Array.length(rule.vars) == Array.length(it.instantiation) => {
-        let {premises,conclusion} = Rule.instantiate(rule,it.instantiation)
-        if Judgment.equivalent(conclusion,j) {
+        let {premises, conclusion} = Rule.instantiate(rule, it.instantiation)
+        if Judgment.equivalent(conclusion, j) {
           if Array.length(it.subgoals) == Array.length(premises) {
             Ok({
               ruleName: it.ruleName,
               instantiation: it.instantiation,
-              subgoals: Belt.Array.zipBy(it.subgoals,premises,f)
+              subgoals: Belt.Array.zipBy(it.subgoals, premises, f),
             })
           } else {
             Error("Incorrect number of subgoals")
           }
         } else {
-          let concString = Judgment.prettyPrint(conclusion,~scope=ctx.fixes)
-          let goalString = Judgment.prettyPrint(j,~scope=ctx.fixes)
-          Error("Conclusion of rule '"
+          let concString = Judgment.prettyPrint(conclusion, ~scope=ctx.fixes)
+          let goalString = Judgment.prettyPrint(j, ~scope=ctx.fixes)
+          Error(
+            "Conclusion of rule '"
             ->String.concat(concString)
             ->String.concat("' doesn't match goal '")
             ->String.concat(goalString)
-            ->String.concat("'"))
+            ->String.concat("'"),
+          )
         }
-      } 
+      }
     | _ => Error("Incorrect number of binders")
     }
   }
 }
-module Lemma = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term
-) => {  
-  module Rule = Rule.Make(Term,Judgment)
-  module Context = Context(Term,Judgment)
+module Lemma = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
+  module Rule = Rule.Make(Term, Judgment)
+  module Context = Context(Term, Judgment)
   type t<'a> = {
     rule: Rule.t,
     proof: 'a,
-    show: 'a
+    show: 'a,
   }
   let uncheck = (it: t<'a>, f) => {
-    { rule: it.rule,
+    {
+      rule: it.rule,
       proof: f(it.proof),
-      show: f(it.show)
+      show: f(it.show),
     }
   }
   let keywords = ["have"]
-  let prettyPrint = (it : t<'a>, ~scope,~indentation=0,
-     ~subprinter: ('a,~scope:array<Term.meta>, ~indentation:int=?)=>string) => {
-    "have "->String.concat(Rule.prettyPrintInline(it.rule,~scope))
-      ->String.concat(newline)
-      ->String.concat(subprinter(it.proof,~scope,~indentation))
-      ->String.concat(newline)
-      ->String.concat(subprinter(it.show,~scope,~indentation))
+  let prettyPrint = (
+    it: t<'a>,
+    ~scope,
+    ~indentation=0,
+    ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string,
+  ) => {
+    "have "
+    ->String.concat(Rule.prettyPrintInline(it.rule, ~scope))
+    ->String.concat(newline)
+    ->String.concat(subprinter(it.proof, ~scope, ~indentation))
+    ->String.concat(newline)
+    ->String.concat(subprinter(it.show, ~scope, ~indentation))
   }
   let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
     //todo add toplevel
     switch Rule.parseInner(input, ~scope, ~gen) {
-    | Ok((rule,rest)) => {
-        switch (subparser(rest,~scope,~gen)) {
-        | Ok((proof,rest')) => 
-          switch String.trim(rest')->subparser(~scope,~gen) {
-          | Ok((show,rest'')) =>  Ok({rule,proof,show}, rest'')
-          | Error(e) => Error(e)
-          }
+    | Ok((rule, rest)) => switch subparser(rest, ~scope, ~gen) {
+      | Ok((proof, rest')) =>
+        switch String.trim(rest')->subparser(~scope, ~gen) {
+        | Ok((show, rest'')) => Ok({rule, proof, show}, rest'')
         | Error(e) => Error(e)
         }
+      | Error(e) => Error(e)
       }
     | Error(e) => Error(e)
     }
   }
-  let check = (it: t<'a>, _ctx : Context.t, j: Judgment.t, f : ('a, Rule.t) => 'b) => {
-    let first = f(it.proof,it.rule)
-    let second = f(it.show,{vars:[],premises:[it.rule],conclusion:j})
-    Ok({rule:it.rule, proof:first, show:second})
+  let check = (it: t<'a>, _ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => {
+    let first = f(it.proof, it.rule)
+    let second = f(it.show, {vars: [], premises: [it.rule], conclusion: j})
+    Ok({rule: it.rule, proof: first, show: second})
   }
 }
 module Combine = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term, 
-  Method1 : PROOF_METHOD with module Term := Term and module Judgment := Judgment,
-  Method2 : PROOF_METHOD with module Term := Term and module Judgment := Judgment
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  Method1: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
+  Method2: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
 ) => {
-  module Rule = Rule.Make(Term,Judgment)
-  module Context = Context(Term,Judgment)
+  module Rule = Rule.Make(Term, Judgment)
+  module Context = Context(Term, Judgment)
   type t<'a> = First(Method1.t<'a>) | Second(Method2.t<'a>)
-  let uncheck = (it, f) => switch it {
-  | First(m) => First(Method1.uncheck(m,f))
-  | Second(m) => Second(Method2.uncheck(m,f))
-  }
-  let keywords = Array.concat(Method1.keywords,Method2.keywords)
-  
-  let check = (it,ctx,  j, f) => switch it {
-  | First(m) => m->Method1.check(ctx,j,f)->Result.map(x => First(x))
-  | Second(m) => m->Method2.check(ctx,j,f)->Result.map(x => Second(x))
-  }
-  let prettyPrint = (it : t<'a>, ~scope, ~indentation=0,~subprinter) => switch it {
-  | First(m) => m->Method1.prettyPrint(~scope,~indentation,~subprinter)
-  | Second(m) => m->Method2.prettyPrint(~scope,~indentation,~subprinter)
-  }
+  let uncheck = (it, f) =>
+    switch it {
+    | First(m) => First(Method1.uncheck(m, f))
+    | Second(m) => Second(Method2.uncheck(m, f))
+    }
+  let keywords = Array.concat(Method1.keywords, Method2.keywords)
+
+  let check = (it, ctx, j, f) =>
+    switch it {
+    | First(m) => m->Method1.check(ctx, j, f)->Result.map(x => First(x))
+    | Second(m) => m->Method2.check(ctx, j, f)->Result.map(x => Second(x))
+    }
+  let prettyPrint = (it: t<'a>, ~scope, ~indentation=0, ~subprinter) =>
+    switch it {
+    | First(m) => m->Method1.prettyPrint(~scope, ~indentation, ~subprinter)
+    | Second(m) => m->Method2.prettyPrint(~scope, ~indentation, ~subprinter)
+    }
   let parse = (input, ~keyword, ~scope, ~gen, ~subparser) => {
     if Method1.keywords->Array.indexOf(keyword) > -1 {
-      Method1.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (First(x),r))
+      Method1.parse(input, ~keyword, ~scope, ~gen, ~subparser)->Result.map(((x, r)) => (
+        First(x),
+        r,
+      ))
     } else {
-      Method2.parse(input,~keyword,~scope,~gen,~subparser)->Result.map(((x,r)) => (Second(x),r))
+      Method2.parse(input, ~keyword, ~scope, ~gen, ~subparser)->Result.map(((x, r)) => (
+        Second(x),
+        r,
+      ))
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/MethodView.res b/src/MethodView.res
index 4ab86df..7bcc90e 100644
--- a/src/MethodView.res
+++ b/src/MethodView.res
@@ -2,71 +2,82 @@ open Util
 open Signatures
 open Method
 module type METHOD_VIEW = {
-  module Term : TERM
-  module Judgment : JUDGMENT with module Term := Term
-  module Method : PROOF_METHOD with 
-    module Term := Term and 
-    module Judgment := Judgment
-  type props<'a> = {method: Method.t<'a>,  scope: array<Term.meta>, ruleStyle: RuleView.style}
+  module Term: TERM
+  module Judgment: JUDGMENT with module Term := Term
+  module Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment
+  type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
   type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
-  let make : (srProps<'a> => React.element) => props<'a> => React.element
+  let make: (srProps<'a> => React.element) => props<'a> => React.element
 }
 
-module DerivationView = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term
-) => {
+module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
   module Method = Derivation(Term, Judgment)
-  type props<'a> = {method: Method.t<'a>,  scope: array<Term.meta>, ruleStyle: RuleView.style}
+  type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
   type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
-  let make = (subRender : srProps<'a> => React.element) => (props) => {
-      <div>
-      <b>{React.string("by ")}</b>
+  let make = (subRender: srProps<'a> => React.element) => props => {
+    <div>
+      <b> {React.string("by ")} </b>
       {React.string(props.method.ruleName)}
       <ul>
-      { props.method.subgoals->Array.mapWithIndex((sg,i) => {
+        {props.method.subgoals
+        ->Array.mapWithIndex((sg, i) => {
           <li key={String.make(i)}>
-            {React.createElement(subRender, {"proof":sg, "scope": props.scope, "ruleStyle": props.ruleStyle})}
+            {React.createElement(
+              subRender,
+              {"proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle},
+            )}
           </li>
-        })->React.array
-      }
+        })
+        ->React.array}
       </ul>
-      </div>
+    </div>
   }
 }
 
 module LemmaView = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term,
-  JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
 ) => {
   module Method = Lemma(Term, Judgment)
-  type props<'a> = {method: Method.t<'a>,  scope: array<Term.meta>, ruleStyle: RuleView.style}
+  type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
   type srProps<'a> = {"proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style}
-  module RuleView = RuleView.Make(Term,Judgment, JudgmentView)
-  let make = (subRender : srProps<'a> => React.element) => (props) => {
-      <div>
-      <b>{React.string("have ")}</b>
-      <RuleView 
-        rule={props.method.rule} 
-        scope={props.scope} 
-        style={props.ruleStyle}> {React.null}
+  module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
+  let make = (subRender: srProps<'a> => React.element) => props => {
+    <div>
+      <b> {React.string("have ")} </b>
+      <RuleView rule={props.method.rule} scope={props.scope} style={props.ruleStyle}>
+        {React.null}
       </RuleView>
-      {React.createElement(subRender,{"proof":props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle})}
-      {React.createElement(subRender,{"proof":props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle})}
-      </div>
+      {React.createElement(
+        subRender,
+        {"proof": props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle},
+      )}
+      {React.createElement(
+        subRender,
+        {"proof": props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle},
+      )}
+    </div>
   }
 }
 module CombineMethodView = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term, 
-  Method1View : METHOD_VIEW with module Term := Term and module Judgment := Judgment,
-  Method2View : METHOD_VIEW with module Term := Term and module Judgment := Judgment and type srProps<'a> = Method1View.srProps<'a>
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  Method1View: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
+  Method2View: METHOD_VIEW
+    with module Term := Term
+    and module Judgment := Judgment
+    and type srProps<'a> = Method1View.srProps<'a>,
 ) => {
-  module Method = Combine(Term,Judgment,Method1View.Method, Method2View.Method)
-  type props<'a> = {method: Method.t<'a>,  scope: array<Term.meta>, ruleStyle: RuleView.style}
+  module Method = Combine(Term, Judgment, Method1View.Method, Method2View.Method)
+  type props<'a> = {method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style}
   type srProps<'a> = Method1View.srProps<'a>
-  let make = (subrender : srProps<'a> => React.element) => (props) => {
+  let make = (subrender: srProps<'a> => React.element) => props => {
     switch props.method {
-    | First(m) => Method1View.make(subrender)({method:m, scope:props.scope, ruleStyle: props.ruleStyle})
-    | Second(m) => Method2View.make(subrender)({method:m, scope:props.scope, ruleStyle: props.ruleStyle})
+    | First(m) =>
+      Method1View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle})
+    | Second(m) =>
+      Method2View.make(subrender)({method: m, scope: props.scope, ruleStyle: props.ruleStyle})
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/Proof.res b/src/Proof.res
index 06a88d2..6733245 100644
--- a/src/Proof.res
+++ b/src/Proof.res
@@ -2,81 +2,94 @@ open Method
 open Signatures
 
 module Make = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term, 
-  Method : PROOF_METHOD with module Term := Term and module Judgment := Judgment
-) => {  
-  module Rule = Rule.Make(Term,Judgment)
-  module Context = Context(Term,Judgment)
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment,
+) => {
+  module Rule = Rule.Make(Term, Judgment)
+  module Context = Context(Term, Judgment)
   type rec t = {
-    fixes: array<Term.meta>, 
+    fixes: array<Term.meta>,
     assumptions: array<string>,
-    method: option<Method.t<t>>
-  }  
-  type rec checked
-    = Checked({
-        fixes: array<Term.meta>, 
+    method: option<Method.t<t>>,
+  }
+  type rec checked =
+    | Checked({
+        fixes: array<Term.meta>,
         assumptions: array<string>,
         method: option<Method.t<checked>>,
-        rule: Rule.t
+        rule: Rule.t,
       })
-    | ProofError({ raw: t, rule: Rule.t, msg: string})
-  let parseKeyword = (input) => {
+    | ProofError({raw: t, rule: Rule.t, msg: string})
+  let parseKeyword = input => {
     Method.keywords
-      ->Array.concat(["?"])
-      ->Array.find(kw => String.trim(input)->String.startsWith(kw))
+    ->Array.concat(["?"])
+    ->Array.find(kw => String.trim(input)->String.startsWith(kw))
   }
-  let rec prettyPrint = (prf : t, ~scope, ~indentation=0) => {
+  let rec prettyPrint = (prf: t, ~scope, ~indentation=0) => {
     let mtd = switch prf.method {
     | None => "?"
-    | Some(m) => Method.prettyPrint(m,
+    | Some(m) =>
+      Method.prettyPrint(
+        m,
         ~scope=prf.fixes->Array.concat(scope),
-        ~indentation=indentation+2,
-        ~subprinter=prettyPrint)
+        ~indentation=indentation + 2,
+        ~subprinter=prettyPrint,
+      )
     }
-    String.padStart("",indentation," ")
-      ->String.concat(prf.fixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
-      ->String.concat(prf.assumptions
-        ->Array.map(s => String.concat(" ", s))
-        ->Array.join(""))
-      ->String.concat(if Array.length(prf.assumptions) == 0 { 
-          "|- " 
-        } else { 
-          " |- "
-        })
-      ->String.concat(mtd)
+    String.padStart("", indentation, " ")
+    ->String.concat(prf.fixes->Array.map(Term.prettyPrintMeta)->Array.join(""))
+    ->String.concat(
+      prf.assumptions
+      ->Array.map(s => String.concat(" ", s))
+      ->Array.join(""),
+    )
+    ->String.concat(
+      if Array.length(prf.assumptions) == 0 {
+        "|- "
+      } else {
+        " |- "
+      },
+    )
+    ->String.concat(mtd)
   }
-  let rec parse = (input, ~scope,~gen) => {
+  let rec parse = (input, ~scope, ~gen) => {
     let it = ref(Error(""))
     let cur = ref(String.trim(input))
     let fixes = []
-    while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
-      let (n,r) = Result.getExn(it.contents)
+    while {
+      it := Term.parseMeta(cur.contents)
+      it.contents->Result.isOk
+    } {
+      let (n, r) = Result.getExn(it.contents)
       cur := String.trim(r)
       fixes->Array.unshift(n)
     }
     let it = ref(Error(""))
     let assumptions = []
-    while {it := Rule.parseRuleName(cur.contents); it.contents->Result.isOk} {
-      let (a,r) = Result.getExn(it.contents)
+    while {
+      it := Rule.parseRuleName(cur.contents)
+      it.contents->Result.isOk
+    } {
+      let (a, r) = Result.getExn(it.contents)
       cur := String.trim(r)
       assumptions->Array.push(a)
     }
-    if cur.contents->String.slice(~start=0,~end=2) != "|-" {
-      Console.log((fixes,assumptions))
+    if cur.contents->String.slice(~start=0, ~end=2) != "|-" {
+      Console.log((fixes, assumptions))
       Error("expected turnstile or rule name"->String.concat(cur.contents))
     } else {
       cur := cur.contents->String.trim->String.sliceToEnd(~start=2)->String.trim
       let scope' = Array.concat(fixes, scope)
       switch parseKeyword(cur.contents) {
-      | Some("?") => {
-          Ok(({fixes,assumptions,method:None},
-            cur.contents->String.sliceToEnd(~start=1)))
-        }
+      | Some("?") => Ok((
+          {fixes, assumptions, method: None},
+          cur.contents->String.sliceToEnd(~start=1),
+        ))
       | Some(keyword) => {
           cur := cur.contents->String.sliceToEnd(~start=String.length(keyword))
-          switch Method.parse(
-            cur.contents, ~keyword,~scope=scope',~gen,~subparser=parse) {
-          | Ok((method,r)) => Ok(({fixes,assumptions,method:Some(method)},r))
+          switch Method.parse(cur.contents, ~keyword, ~scope=scope', ~gen, ~subparser=parse) {
+          | Ok((method, r)) => Ok(({fixes, assumptions, method: Some(method)}, r))
           | Error(e) => Error(e)
           }
         }
@@ -84,13 +97,13 @@ module Make = (
       }
     }
   }
-  let enter = (ctx : Context.t, prf: t, rule: Rule.t) => {
+  let enter = (ctx: Context.t, prf: t, rule: Rule.t) => {
     if Array.length(prf.fixes) == Array.length(rule.vars) {
       if Array.length(prf.assumptions) == Array.length(rule.premises) {
-        let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions,rule.premises))
-        Ok({ 
+        let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions, rule.premises))
+        Ok({
           Context.fixes: rule.vars->Array.concat(ctx.fixes),
-          facts: Dict.copy(ctx.facts)->Dict.assign(newFacts)
+          facts: Dict.copy(ctx.facts)->Dict.assign(newFacts),
         })
       } else {
         Error("Proof introduces a different number of assumptions than the rule")
@@ -98,42 +111,49 @@ module Make = (
     } else {
       Error("Proof introduces a different number of variables than the rule")
     }
-  
   } //result<Context, string>
-  
-  let rec uncheck = (prf : checked) => switch prf {
-  | ProofError({ raw, rule:_, msg:_ }) => raw
-  | Checked({fixes,assumptions,method,rule:_}) => {
-      fixes, assumptions, 
-      method: method->Option.map(xs => xs->Method.uncheck(uncheck))
+
+  let rec uncheck = (prf: checked) =>
+    switch prf {
+    | ProofError({raw, rule: _, msg: _}) => raw
+    | Checked({fixes, assumptions, method, rule: _}) => {
+        fixes,
+        assumptions,
+        method: method->Option.map(xs => xs->Method.uncheck(uncheck)),
+      }
     }
-  }
-  let rec check = (ctx : Context.t, prf: t, rule: Rule.t) => {
-    let ruleStr = Rule.prettyPrintInline(rule,~scope=[])
-    Console.log(("CHECK",ctx,prf,ruleStr))
-    switch enter(ctx,prf,rule) {
-    | Ok(ctx') => switch prf.method {
+  let rec check = (ctx: Context.t, prf: t, rule: Rule.t) => {
+    let ruleStr = Rule.prettyPrintInline(rule, ~scope=[])
+    Console.log(("CHECK", ctx, prf, ruleStr))
+    switch enter(ctx, prf, rule) {
+    | Ok(ctx') =>
+      switch prf.method {
       | Some(m) =>
-        switch m->Method.check(ctx', rule.conclusion, (s, r) => check(ctx',s,r)) {
-        | Ok(m') => Checked({
-            rule, fixes: prf.fixes, 
-            assumptions: prf.assumptions, 
-            method:Some(m')
+        switch m->Method.check(ctx', rule.conclusion, (s, r) => check(ctx', s, r)) {
+        | Ok(m') =>
+          Checked({
+            rule,
+            fixes: prf.fixes,
+            assumptions: prf.assumptions,
+            method: Some(m'),
           })
-        | Error(e) => ProofError({raw:prf, rule, msg:e}) 
+        | Error(e) => ProofError({raw: prf, rule, msg: e})
         }
-      | None => Checked({
-          rule, fixes: prf.fixes, assumptions: prf.assumptions, method: None
+      | None =>
+        Checked({
+          rule,
+          fixes: prf.fixes,
+          assumptions: prf.assumptions,
+          method: None,
         })
       }
-    | Error(e) => ProofError({raw:prf, rule, msg: e})
+    | Error(e) => ProofError({raw: prf, rule, msg: e})
     }
-  }// result<checked,string>
-
+  } // result<checked,string>
 }
 
-  /* 
+/*
   
     
   
-  */
+ */
diff --git a/src/ProofView.res b/src/ProofView.res
index 54a74aa..679efaf 100644
--- a/src/ProofView.res
+++ b/src/ProofView.res
@@ -3,55 +3,51 @@ open Method
 open MethodView
 
 module Make = (
-  Term : TERM, Judgment : JUDGMENT with module Term := Term, 
-  JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
-  MethodView : METHOD_VIEW with module Term := Term and module Judgment := Judgment
-) => {  
-  module Rule = Rule.Make(Term, Judgment)  
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
+  MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
+) => {
+  module Rule = Rule.Make(Term, Judgment)
   module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
   module Proof = Proof.Make(Term, Judgment, MethodView.Method)
-  
+
   type props = {
-    proof: Proof.checked, 
-    scope: array<Term.meta>, 
-    ruleStyle: RuleView.style
+    proof: Proof.checked,
+    scope: array<Term.meta>,
+    ruleStyle: RuleView.style,
   }
   module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
   @react.componentWithProps
-  let rec make = (props : props) => {
+  let rec make = (props: props) => {
     switch props.proof {
     | Proof.Checked({fixes, assumptions, method, rule}) => {
-        let scope = Array.concat(fixes,props.scope)
+        let scope = Array.concat(fixes, props.scope)
         <>
-        <ScopeView scope=fixes />
-        <ul className="proof-assumptions">
-          { Belt.Array.zipBy(assumptions,rule.premises, (n,r) => {
+          <ScopeView scope=fixes />
+          <ul className="proof-assumptions">
+            {Belt.Array.zipBy(assumptions, rule.premises, (n, r) => {
               <li key={n}>
-                <RuleView rule=r style=props.ruleStyle scope>
-                {React.string(n)}
-                </RuleView> 
+                <RuleView rule=r style=props.ruleStyle scope> {React.string(n)} </RuleView>
               </li>
-            })->React.array
-          }
-        </ul>
-        <div className="proof-show"> 
-          <JudgmentView judgment={rule.conclusion} scope />
-          {
-            switch method {
+            })->React.array}
+          </ul>
+          <div className="proof-show">
+            <JudgmentView judgment={rule.conclusion} scope />
+            {switch method {
             | None => React.null
-            | Some(method) => React.createElement(
-                MethodView.make(p => make({proof: p["proof"], scope: p["scope"], ruleStyle:p["ruleStyle"] })), 
-                  {method, scope, ruleStyle: props.ruleStyle})
-            }
-          }
-        </div>
+            | Some(method) =>
+              React.createElement(
+                MethodView.make(p =>
+                  make({proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"]})
+                ),
+                {method, scope, ruleStyle: props.ruleStyle},
+              )
+            }}
+          </div>
         </>
       }
-    | Proof.ProofError({raw:_, rule:_, msg}) => {
-        <div className="error">{React.string(msg)}</div>
-      }
-  
+    | Proof.ProofError({raw: _, rule: _, msg}) => <div className="error"> {React.string(msg)} </div>
     }
   }
-
-}
\ No newline at end of file
+}
diff --git a/src/Rule.res b/src/Rule.res
index 3922f74..32d5a4b 100644
--- a/src/Rule.res
+++ b/src/Rule.res
@@ -3,103 +3,109 @@ open Signatures
 // level..
 let ruleNamePattern = "^[^|()\\s\\-—][^()\\s]*"
 let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?"
-module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
+module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
   type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t}
   let rec substitute = (rule: t, subst: Term.subst) => {
-    let subst' = subst->Util.mapMapValues(v => v->Term.upshift(Array.length(rule.vars)));
-    { 
-      vars: rule.vars, 
+    let subst' = subst->Util.mapMapValues(v => v->Term.upshift(Array.length(rule.vars)))
+    {
+      vars: rule.vars,
       premises: rule.premises->Array.map(premise => premise->substitute(subst')),
-      conclusion: rule.conclusion->Judgment.substitute(subst')
+      conclusion: rule.conclusion->Judgment.substitute(subst'),
     }
   }
-  let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from:int=0) => {
+  let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from: int=0) => {
     let len = Array.length(rule.vars)
-    let substs' = substs->Array.map(v => v->Term.upshift(len,~from=from))
+    let substs' = substs->Array.map(v => v->Term.upshift(len, ~from))
     {
       vars: rule.vars,
-      premises: rule.premises
-        ->Array.map(premise => premise->substDeBruijn(substs', ~from=from+len)),
-      conclusion: rule.conclusion
-        ->Judgment.substDeBruijn(substs',~from=from+len),
+      premises: rule.premises->Array.map(premise =>
+        premise->substDeBruijn(substs', ~from=from + len)
+      ),
+      conclusion: rule.conclusion->Judgment.substDeBruijn(substs', ~from=from + len),
     }
   }
-  let rec upshift = (rule: t, amount: int, ~from:int=0) => {
+  let rec upshift = (rule: t, amount: int, ~from: int=0) => {
     let len = Array.length(rule.vars)
     {
       vars: rule.vars,
-      premises: rule.premises->Array.map(r => r->upshift(amount, ~from = from + len)),
-      conclusion: rule.conclusion->Judgment.upshift(amount, ~from = from + len)
+      premises: rule.premises->Array.map(r => r->upshift(amount, ~from=from + len)),
+      conclusion: rule.conclusion->Judgment.upshift(amount, ~from=from + len),
     }
   }
-  type bare = { premises: array<t>, conclusion: Judgment.t }
+  type bare = {premises: array<t>, conclusion: Judgment.t}
   let instantiate = (rule: t, terms: array<Term.t>) => {
     assert(Array.length(terms) == Array.length(rule.vars))
     let terms' = [...terms]
     Array.reverse(terms')
     {
-      premises: rule.premises->Array.map(r => r-> substDeBruijn(terms')),
-      conclusion: rule.conclusion->Judgment.substDeBruijn(terms')
+      premises: rule.premises->Array.map(r => r->substDeBruijn(terms')),
+      conclusion: rule.conclusion->Judgment.substDeBruijn(terms'),
     }
   }
-  let parseRuleName = (str) => {
-    let re = RegExp.fromStringWithFlags(ruleNamePattern,~flags="y")
+  let parseRuleName = str => {
+    let re = RegExp.fromStringWithFlags(ruleNamePattern, ~flags="y")
     switch re->RegExp.exec(String.trim(str)) {
     | None => Error("expected rule name")
-    | Some(res) => { switch res[0] {
-      | Some(Some(n)) if String.trim(n) != "" 
-          => Ok(n,String.sliceToEnd(String.trim(str),~start=RegExp.lastIndex(re)))
+    | Some(res) => switch res[0] {
+      | Some(Some(n)) if String.trim(n) != "" =>
+        Ok(n, String.sliceToEnd(String.trim(str), ~start=RegExp.lastIndex(re)))
       | _ => Error("expected rule name")
-      }}
+      }
     }
   }
-  let parseVinculum = (str) => {
-    let re = RegExp.fromStringWithFlags(vinculumRES,~flags="y")
+  let parseVinculum = str => {
+    let re = RegExp.fromStringWithFlags(vinculumRES, ~flags="y")
     switch re->RegExp.exec(str) {
     | None => Error("expected vinculum")
-    | Some(res) => { switch res[1] {
-      | Some(Some(n)) if String.trim(n) != "" 
-          => Ok(n,String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
-      | _ => Ok("", String.sliceToEnd(str,~start=RegExp.lastIndex(re)))
-      }}
+    | Some(res) => switch res[1] {
+      | Some(Some(n)) if String.trim(n) != "" =>
+        Ok(n, String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
+      | _ => Ok("", String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))
+      }
     }
   }
   exception InternalParseError(string)
   let rec parseInner = (string, ~scope=[]: array<Term.meta>, ~gen=?) => {
-    if (string->String.trim->String.get(0) == Some("[")) {
-      let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)));
+    if string->String.trim->String.get(0) == Some("[") {
+      let cur = ref(String.make(string->String.trim->String.sliceToEnd(~start=1)))
       let it = ref(Error(""))
       let vars = []
-      while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
-        let (str,rest) = Result.getExn(it.contents)
-        Array.unshift(vars,str)
+      while {
+        it := Term.parseMeta(cur.contents)
+        it.contents->Result.isOk
+      } {
+        let (str, rest) = Result.getExn(it.contents)
+        Array.unshift(vars, str)
         cur := rest
       }
       let premises = []
-      switch {  
-        while (cur.contents->String.trim->String.slice(~start=0,~end=2) != "|-" 
-          && cur.contents->String.trim->String.get(0) != Some("]")) {
-          switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
-          | Ok(p,rest) => {
+      switch {
+        while (
+          cur.contents->String.trim->String.slice(~start=0, ~end=2) != "|-" &&
+            cur.contents->String.trim->String.get(0) != Some("]")
+        ) {
+          switch parseInner(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
+          | Ok(p, rest) => {
               cur := rest
               premises->Array.push(p)
             }
           | Error(_) => raise(InternalParseError("expected turnstile or premise"))
           }
         }
-        if (cur.contents->String.trim->String.get(0) == Some("]")) {
+        if cur.contents->String.trim->String.get(0) == Some("]") {
           let rest = cur.contents->String.trim->String.sliceToEnd(~start=1)
           cur := rest
           switch premises {
-          | [{vars:[],premises:[],conclusion:e}] => Ok(({vars,premises:[],conclusion:e}, rest))
+          | [{vars: [], premises: [], conclusion: e}] =>
+            Ok(({vars, premises: [], conclusion: e}, rest))
           | _ => Error("Conclusion appears to be multiple terms")
           }
         } else {
           cur := cur.contents->String.trim->String.sliceToEnd(~start=2)
-          switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
+          switch Judgment.parse(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
           | Ok(conclusion, rest) =>
-            if (rest->String.trim->String.get(0) == Some("]")) {
-              cur := rest->String.trim->String.sliceToEnd(~start=1);
+            if rest->String.trim->String.get(0) == Some("]") {
+              cur := rest->String.trim->String.sliceToEnd(~start=1)
               Ok(({vars, premises, conclusion}, cur.contents))
             } else {
               Error("Expected closing bracket")
@@ -111,37 +117,43 @@ module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
       | exception InternalParseError(e) => Error(e)
       | v => v
       }
-    } else { 
-      switch Judgment.parse(string,~scope,~gen=?gen) {
-      | Ok(conclusion, rest) => Ok(({vars:[], premises:[], conclusion}, rest))
+    } else {
+      switch Judgment.parse(string, ~scope, ~gen?) {
+      | Ok(conclusion, rest) => Ok(({vars: [], premises: [], conclusion}, rest))
       | Error(e) => Error(e)
       }
     }
   }
   let parseTopLevel = (string, ~gen=?, ~scope=[]) => {
-    let cur = ref(String.make(string));
+    let cur = ref(String.make(string))
     let it = ref(Error(""))
     let vars = []
     switch {
-      while {it := Term.parseMeta(cur.contents); it.contents->Result.isOk} {
-        let (str,rest) = Result.getExn(it.contents)
-        Array.unshift(vars,str)
+      while {
+        it := Term.parseMeta(cur.contents)
+        it.contents->Result.isOk
+      } {
+        let (str, rest) = Result.getExn(it.contents)
+        Array.unshift(vars, str)
         cur := rest
       }
       let it = ref(Error(""))
       let premises = []
-      while {it := parseVinculum(cur.contents); it.contents->Result.isError} {
-        switch parseInner(cur.contents,~scope=vars->Array.concat(scope), ~gen=?gen) {
-        | Ok(p,rest) => {
+      while {
+        it := parseVinculum(cur.contents)
+        it.contents->Result.isError
+      } {
+        switch parseInner(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
+        | Ok(p, rest) => {
             cur := rest
             premises->Array.push(p)
           }
         | Error(e) => raise(InternalParseError(e))
         }
       }
-      let (ruleName,rest) = it.contents->Result.getExn
+      let (ruleName, rest) = it.contents->Result.getExn
       cur := rest
-      switch Judgment.parse(cur.contents,~scope=vars->Array.concat(scope),~gen=?gen) {
+      switch Judgment.parse(cur.contents, ~scope=vars->Array.concat(scope), ~gen?) {
       | Ok(conclusion, rest) => Ok((({vars, premises, conclusion}, ruleName), rest))
       | Error(e) => Error(e)
       }
@@ -150,50 +162,58 @@ module Make = (Term : TERM, Judgment : JUDGMENT with module Term := Term) => {
     | v => v
     }
   }
-  
-  let rec prettyPrintInline = (rule: t,~scope=[]:array<Term.meta>) => {
+
+  let rec prettyPrintInline = (rule: t, ~scope=[]: array<Term.meta>) => {
     switch rule {
-    | {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c,~scope)
+    | {vars: [], premises: [], conclusion: c} => Judgment.prettyPrint(c, ~scope)
     | _ => {
-      let vars' = Array.copy(rule.vars)
-      Array.reverse(vars')
-      "["->String.concat(vars'
-        ->Array.map(Term.prettyPrintMeta)
-        ->Array.join("")
-        ->String.concat(" ")
-        ->String.concat(if Array.length(rule.premises) == 0 {
-            Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope])
-          } else {
-            rule.premises
-              ->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))->Array.join(" ")
+        let vars' = Array.copy(rule.vars)
+        Array.reverse(vars')
+        "["
+        ->String.concat(
+          vars'
+          ->Array.map(Term.prettyPrintMeta)
+          ->Array.join("")
+          ->String.concat(" ")
+          ->String.concat(
+            if Array.length(rule.premises) == 0 {
+              Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope])
+            } else {
+              rule.premises
+              ->Array.map(r => prettyPrintInline(r, ~scope=[...rule.vars, ...scope]))
+              ->Array.join(" ")
               ->String.concat(" |- ")
-              ->String.concat(Judgment.prettyPrint(rule.conclusion,~scope=[...rule.vars,...scope]))
-          }
-        ))->String.concat("]")
+              ->String.concat(
+                Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope]),
+              )
+            },
+          ),
+        )
+        ->String.concat("]")
       }
     }
   }
-  let prettyPrintTopLevel = (rule: t,~name="",~scope=[]:array<Term.meta>) => {
+  let prettyPrintTopLevel = (rule: t, ~name="", ~scope=[]: array<Term.meta>) => {
     let vinculise = (strs: array<string>) => {
       let l = strs->Array.map(String.length)->Array.concat([4])->Math.Int.maxMany
       strs->Array.concat(["-"->String.repeat(l)->String.concat(" ")->String.concat(name)])
     }
-    let myReverse = (arr) => {
+    let myReverse = arr => {
       Array.reverse(arr)
       arr
     }
     rule.vars
-      ->Array.map(Term.prettyPrintMeta)
-      ->myReverse
-      ->Array.join("")
-      ->String.concat(Util.newline)
-      ->String.concat(
-          rule.premises
-            ->Array.map(r => prettyPrintInline(r,~scope=[...rule.vars,...scope]))
-            ->vinculise
-            ->Array.concat([Judgment.prettyPrint(rule.conclusion,
-                ~scope=[...rule.vars,...scope])])
-            ->Array.map(s => String.concat("  ",s))
-            ->Array.join(Util.newline))
+    ->Array.map(Term.prettyPrintMeta)
+    ->myReverse
+    ->Array.join("")
+    ->String.concat(Util.newline)
+    ->String.concat(
+      rule.premises
+      ->Array.map(r => prettyPrintInline(r, ~scope=[...rule.vars, ...scope]))
+      ->vinculise
+      ->Array.concat([Judgment.prettyPrint(rule.conclusion, ~scope=[...rule.vars, ...scope])])
+      ->Array.map(s => String.concat("  ", s))
+      ->Array.join(Util.newline),
+    )
   }
 }
diff --git a/src/RuleView.res b/src/RuleView.res
index ec3b3e0..fff601c 100644
--- a/src/RuleView.res
+++ b/src/RuleView.res
@@ -2,117 +2,147 @@ open Signatures
 open Util
 type style = Gentzen | Linear | Hybrid
 module Make = (
-  Term : TERM,
-  Judgment : JUDGMENT with module Term := Term,
-  JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
 ) => {
-  module Rule = Rule.Make(Term, Judgment)  
+  module Rule = Rule.Make(Term, Judgment)
   module ScopeView = ScopeView.Make(Term, JudgmentView.TermView)
   type props = {
-    rule:Rule.t, 
-    style: style, 
-    scope?: array<Term.meta>, 
-    children: React.element
+    rule: Rule.t,
+    style: style,
+    scope?: array<Term.meta>,
+    children: React.element,
   }
   module type RULE_COMPONENT = {
-    let make : props => React.element
+    let make: props => React.element
   }
-  module Inline : RULE_COMPONENT = {
-    let rec make = (props : props) => {
-      let {vars, premises,conclusion} = props.rule
+  module Inline: RULE_COMPONENT = {
+    let rec make = (props: props) => {
+      let {vars, premises, conclusion} = props.rule
       let scope = vars->Array.concat(props.scope->Option.getOr([]))
       <span className="inline-rule">
-        <span className="rule-rulename-defined">
-        {props.children}
-        </span>
+        <span className="rule-rulename-defined"> {props.children} </span>
         <ScopeView scope=vars />
-        {React.array(premises
-          ->Array.mapWithIndex((p,i)=><span key={String.make(i)} className="rule-context">
-              {React.createElement(make,withKey({rule:p, scope,children:React.string(""),style:props.style}, i))}</span>)
-          ->Array.flatMapWithIndex( (e, i) => 
-              if i == 0 {
-                [e]
-              } else {
-                [<span key={String.make(-i)} className="symbol symbol-bold symbol-comma">{React.string(",")}</span>,e]
-              }))}
-        {if premises->Array.length > 0 { 
-          <span className="symbol symbol-turnstile symbol-bold">
-            {React.string("⊢")}
-          </span> 
-        } else { 
+        {React.array(
+          premises
+          ->Array.mapWithIndex((p, i) =>
+            <span key={String.make(i)} className="rule-context">
+              {React.createElement(
+                make,
+                withKey({rule: p, scope, children: React.string(""), style: props.style}, i),
+              )}
+            </span>
+          )
+          ->Array.flatMapWithIndex((e, i) =>
+            if i == 0 {
+              [e]
+            } else {
+              [
+                <span key={String.make(-i)} className="symbol symbol-bold symbol-comma">
+                  {React.string(",")}
+                </span>,
+                e,
+              ]
+            }
+          ),
+        )}
+        {if premises->Array.length > 0 {
+          <span className="symbol symbol-turnstile symbol-bold"> {React.string("⊢")} </span>
+        } else {
           React.string("")
         }}
-        <JudgmentView judgment={conclusion} 
-          scope={scope} />
+        <JudgmentView judgment={conclusion} scope={scope} />
       </span>
     }
   }
-  module Hypothetical = (Premise : RULE_COMPONENT) => {
-    let make = (props : props) => if Array.length(props.rule.premises) == 0 { Inline.make(props) } else {
-      let {vars, premises,conclusion} = props.rule
-      let scope = vars->Array.concat(props.scope->Option.getOr([]))
-      <table className="inference"><tbody>
-      <tr><td className="rule-cell rule-binderbox" rowSpan=3>
-      <ScopeView scope=vars/></td>
-        {React.array(premises->Array.mapWithIndex((p,i)=>
-          <td className="rule-cell rule-premise" key={String.make(i)}>
-            <Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
-              {React.string("")}
-            </Premise>
-          </td>))}
-        <td className="rule-cell rule-spacer"></td>
-        <td rowSpan=3 className="rule-cell rule-rulebox">
-          <span className="rule-rulename-defined">
-            {props.children}
-          </span>
-        </td>
-      </tr>
-      <tr> <td colSpan={premises->Array.length + 1} className="rule-cell">
-        {React.string("⋮")}
-      </td></tr>
-      <tr>
-        <td colSpan={premises->Array.length + 1} className="rule-cell rule-hypothetical-conclusion">
-          <JudgmentView judgment={conclusion} scope={scope} />
-        </td>
-      </tr></tbody></table>
-    }
+  module Hypothetical = (Premise: RULE_COMPONENT) => {
+    let make = (props: props) =>
+      if Array.length(props.rule.premises) == 0 {
+        Inline.make(props)
+      } else {
+        let {vars, premises, conclusion} = props.rule
+        let scope = vars->Array.concat(props.scope->Option.getOr([]))
+        <table className="inference">
+          <tbody>
+            <tr>
+              <td className="rule-cell rule-binderbox" rowSpan=3>
+                <ScopeView scope=vars />
+              </td>
+              {React.array(
+                premises->Array.mapWithIndex((p, i) =>
+                  <td className="rule-cell rule-premise" key={String.make(i)}>
+                    <Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
+                      {React.string("")}
+                    </Premise>
+                  </td>
+                ),
+              )}
+              <td className="rule-cell rule-spacer" />
+              <td rowSpan=3 className="rule-cell rule-rulebox">
+                <span className="rule-rulename-defined"> {props.children} </span>
+              </td>
+            </tr>
+            <tr>
+              <td colSpan={premises->Array.length + 1} className="rule-cell">
+                {React.string("⋮")}
+              </td>
+            </tr>
+            <tr>
+              <td
+                colSpan={premises->Array.length + 1}
+                className="rule-cell rule-hypothetical-conclusion">
+                <JudgmentView judgment={conclusion} scope={scope} />
+              </td>
+            </tr>
+          </tbody>
+        </table>
+      }
   }
-  module TopLevel = (Premise : RULE_COMPONENT) => {
-    let make = (props : props) => {
-      let {vars, premises,conclusion} = props.rule
+  module TopLevel = (Premise: RULE_COMPONENT) => {
+    let make = (props: props) => {
+      let {vars, premises, conclusion} = props.rule
       let scope = vars->Array.concat(props.scope->Option.getOr([]))
-      <div className="axiom"><table className="inference"><tbody>
-      <tr><td className="rule-cell rule-binderbox" rowSpan=2>
-      <ScopeView scope=vars/></td>
-        {React.array(premises->Array.mapWithIndex((p,i)=>
-          <td className="rule-cell rule-premise" key={String.make(i)}>
-            <Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
-              {React.string("")}
-            </Premise>
-          </td>))}
-        <td className="rule-cell rule-spacer"></td>
-        <td rowSpan=2 className="rule-cell rule-rulebox">
-          <span className="rule-rulename-defined">
-            {props.children}
-          </span>
-        </td>
-      </tr>
-      <tr>
-        <td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
-          <JudgmentView judgment={conclusion} scope={scope} />
-        </td>
-      </tr></tbody></table></div>
+      <div className="axiom">
+        <table className="inference">
+          <tbody>
+            <tr>
+              <td className="rule-cell rule-binderbox" rowSpan=2>
+                <ScopeView scope=vars />
+              </td>
+              {React.array(
+                premises->Array.mapWithIndex((p, i) =>
+                  <td className="rule-cell rule-premise" key={String.make(i)}>
+                    <Premise rule={p} scope={scope} key={String.make(i)} style={props.style}>
+                      {React.string("")}
+                    </Premise>
+                  </td>
+                ),
+              )}
+              <td className="rule-cell rule-spacer" />
+              <td rowSpan=2 className="rule-cell rule-rulebox">
+                <span className="rule-rulename-defined"> {props.children} </span>
+              </td>
+            </tr>
+            <tr>
+              <td colSpan={premises->Array.length + 1} className="rule-cell rule-conclusion">
+                <JudgmentView judgment={conclusion} scope={scope} />
+              </td>
+            </tr>
+          </tbody>
+        </table>
+      </div>
     }
   }
   module Gentzen = TopLevel(Hypothetical(Inline))
   module Hybrid = TopLevel(Inline)
-  
+
   @react.componentWithProps
-  let make = (props) => {
-    switch (props.style) {
+  let make = props => {
+    switch props.style {
     | Hybrid => Hybrid.make(props)
     | Gentzen => Gentzen.make(props)
     | Linear => Inline.make(props)
     }
   }
-} 
+}
diff --git a/src/SExp.res b/src/SExp.res
index 0350b35..0eff0c1 100644
--- a/src/SExp.res
+++ b/src/SExp.res
@@ -1,193 +1,228 @@
-module IntCmp = Belt.Id.MakeComparable({type t = int;let cmp = Pervasives.compare })
+module IntCmp = Belt.Id.MakeComparable({
+  type t = int
+  let cmp = Pervasives.compare
+})
 
 type rec t =
-    Symbol({name: string }) 
-  | Compound({subexps: array<t>}) 
-  | Var({idx:int}) 
-  | Schematic({schematic:int, allowed: array<int>})
+  | Symbol({name: string})
+  | Compound({subexps: array<t>})
+  | Var({idx: int})
+  | Schematic({schematic: int, allowed: array<int>})
 type meta = string
 type schematic = int
-type subst = Map.t<schematic,t>
-let equivalent = (a : t, b: t) => {
+type subst = Map.t<schematic, t>
+let equivalent = (a: t, b: t) => {
   a == b
 }
-let rec schematicsIn : (t) => Belt.Set.t<int, IntCmp.identity> = (it : t) => switch it {
-| Schematic({schematic,_}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
-| Compound({subexps}) => subexps->Array.reduce(
-    Belt.Set.make(~id=module(IntCmp)), 
-    (s, x) => Belt.Set.union(s, schematicsIn(x))
-  )
-| _ => Belt.Set.make(~id=module(IntCmp))
-}
-let rec freeVarsIn : (t) => Belt.Set.t<int, IntCmp.identity> = (it : t) => switch it {
-| Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
-| Compound({subexps}) => subexps->Array.reduce(
-    Belt.Set.make(~id=module(IntCmp)), 
-    (s, x) => Belt.Set.union(s, freeVarsIn(x))
-  )
-| _ => Belt.Set.make(~id=module(IntCmp))
-}
-let rec substitute = (term: t, subst: subst) => switch term {
-| Compound({subexps}) => 
-    Compound({subexps: Array.map(subexps, x => substitute(x,subst))})
-| Schematic({schematic, _}) => switch Map.get(subst,schematic) {
-  | None => term
-  | Some(found) => found
+let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
+  switch it {
+  | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic)
+  | Compound({subexps}) =>
+    subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
+      Belt.Set.union(s, schematicsIn(x))
+    )
+  | _ => Belt.Set.make(~id=module(IntCmp))
+  }
+let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) =>
+  switch it {
+  | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx)
+  | Compound({subexps}) =>
+    subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) =>
+      Belt.Set.union(s, freeVarsIn(x))
+    )
+  | _ => Belt.Set.make(~id=module(IntCmp))
+  }
+let rec substitute = (term: t, subst: subst) =>
+  switch term {
+  | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))})
+  | Schematic({schematic, _}) =>
+    switch Map.get(subst, schematic) {
+    | None => term
+    | Some(found) => found
+    }
+  | _ => term
   }
-| _ => term
-}
 
-let combineSubst = (s : subst, t: subst) => {
-  let nu = Map.make();
-  Map.entries(s)->Iterator.forEach(opt => switch opt {
-  | None => ()
-  | Some((key,term)) => nu->Map.set(key, term->substitute(t))
-  })
-  Map.entries(t)->Iterator.forEach(opt => switch opt {
-  | None => ()
-  | Some((key,term)) => nu->Map.set(key, term->substitute(s))
-  })
+let combineSubst = (s: subst, t: subst) => {
+  let nu = Map.make()
+  Map.entries(s)->Iterator.forEach(opt =>
+    switch opt {
+    | None => ()
+    | Some((key, term)) => nu->Map.set(key, term->substitute(t))
+    }
+  )
+  Map.entries(t)->Iterator.forEach(opt =>
+    switch opt {
+    | None => ()
+    | Some((key, term)) => nu->Map.set(key, term->substitute(s))
+    }
+  )
   nu
 }
-let emptySubst : subst = Map.make()
-let singletonSubst : (int, t) => subst = (schematic,term) => {
+let emptySubst: subst = Map.make()
+let singletonSubst: (int, t) => subst = (schematic, term) => {
   let s = Map.make()
-  s->Map.set(schematic,term)
+  s->Map.set(schematic, term)
   s
 }
-let rec unifyTerm = (a: t, b: t) => switch (a,b) {
-| (Symbol({name:na}), Symbol({name:nb})) if na == nb => Some(emptySubst)
-| (Var({idx:ia}), Var({idx:ib})) if ia == ib => Some(emptySubst)
-| (Schematic({schematic:sa,_}), Schematic({schematic:sb,_})) if sa == sb => Some(emptySubst)
-| (Compound({subexps:xa}), Compound({subexps:xb})) if Array.length(xa) == Array.length(xb) =>
-  unifyArray(Belt.Array.zip(xa,xb))
-| (Schematic({schematic,allowed}), t)
-  if !Belt.Set.has(schematicsIn(t), schematic)
-  && Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed,~id=module(IntCmp))) 
-  => Some(singletonSubst(schematic,t))
-| (t, Schematic({schematic,allowed}))
-  if !Belt.Set.has(schematicsIn(t), schematic)
-  && Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed,~id=module(IntCmp)))
-  => Some(singletonSubst(schematic,t))
-| (_,_) => None
-}
-and unifyArray = (a: array<(t,t)>) => {
-  if (Array.length(a) == 0) {
+let rec unifyTerm = (a: t, b: t) =>
+  switch (a, b) {
+  | (Symbol({name: na}), Symbol({name: nb})) if na == nb => Some(emptySubst)
+  | (Var({idx: ia}), Var({idx: ib})) if ia == ib => Some(emptySubst)
+  | (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb => Some(emptySubst)
+  | (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) =>
+    unifyArray(Belt.Array.zip(xa, xb))
+  | (Schematic({schematic, allowed}), t)
+    if !Belt.Set.has(schematicsIn(t), schematic) &&
+    Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
+    Some(singletonSubst(schematic, t))
+  | (t, Schematic({schematic, allowed}))
+    if !Belt.Set.has(schematicsIn(t), schematic) &&
+    Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) =>
+    Some(singletonSubst(schematic, t))
+  | (_, _) => None
+  }
+and unifyArray = (a: array<(t, t)>) => {
+  if Array.length(a) == 0 {
     Some(emptySubst)
   } else {
-    let (x,y) = a[0]->Option.getUnsafe
-    switch unifyTerm(x,y) {
-    | None     => None
-    | Some(s1) => {
-        switch a
-          ->Array.sliceToEnd(~start=1)
-          ->Array.map(((t1,t2)) => (substitute(t1,s1),substitute(t2,s1)))
-          ->unifyArray {
-        | None     => None
-        | Some(s2) => Some(combineSubst(s1,s2))
-        }
+    let (x, y) = a[0]->Option.getUnsafe
+    switch unifyTerm(x, y) {
+    | None => None
+    | Some(s1) => switch a
+      ->Array.sliceToEnd(~start=1)
+      ->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
+      ->unifyArray {
+      | None => None
+      | Some(s2) => Some(combineSubst(s1, s2))
       }
     }
   }
 }
 let unify = (a: t, b: t) => {
-  switch unifyTerm(a,b) {
+  switch unifyTerm(a, b) {
   | None => []
   | Some(s) => [s]
   }
 }
-let rec substDeBruijn = (term: t, substs: array<t>, ~from:int=0) => switch term {
-| Symbol(_) => term
-| Compound({subexps}) => 
-    Compound({subexps: Array.map(subexps, x => substDeBruijn(x,substs,~from=from))})
-| Var({idx:var}) => if (var < from) {
-    term
-  } else if (var - from < Array.length(substs) && var - from >= 0) {
-    Option.getUnsafe(substs[var - from])
-  } else {
-    Var({idx: var - Array.length(substs) })
-  }
-| Schematic({schematic,allowed}) =>
-    Schematic({schematic, allowed: 
-      Array.filterMap(allowed, i =>
-        if (i < from + Array.length(substs)) { 
-          None 
-        } else { 
+let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) =>
+  switch term {
+  | Symbol(_) => term
+  | Compound({subexps}) =>
+    Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
+  | Var({idx: var}) =>
+    if var < from {
+      term
+    } else if var - from < Array.length(substs) && var - from >= 0 {
+      Option.getUnsafe(substs[var - from])
+    } else {
+      Var({idx: var - Array.length(substs)})
+    }
+  | Schematic({schematic, allowed}) =>
+    Schematic({
+      schematic,
+      allowed: Array.filterMap(allowed, i =>
+        if i < from + Array.length(substs) {
+          None
+        } else {
           Some(i - (from + Array.length(substs)))
         }
-      )
+      ),
     })
-}
-let rec upshift = (term: t, amount: int, ~from:int=0) => switch term {
-| Symbol(_) => term
-| Compound({subexps}) => 
-    Compound({subexps: Array.map(subexps, x => upshift(x,amount,~from=from))})
-| Var({idx}) => Var({idx: if (idx >= from) { idx + amount } else { idx }})
-| Schematic({schematic,allowed}) =>
-    Schematic({schematic, allowed: 
-      Array.map(allowed, i => if (i >= from) { i + amount } else { i })
+  }
+let rec upshift = (term: t, amount: int, ~from: int=0) =>
+  switch term {
+  | Symbol(_) => term
+  | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))})
+  | Var({idx}) =>
+    Var({
+      idx: if idx >= from {
+        idx + amount
+      } else {
+        idx
+      },
     })
-}
-let place = (x : int,~scope: array<string>)
-  => Schematic({schematic:x,allowed: Array.fromInitializer(~length=Array.length(scope), i=>i)})
+  | Schematic({schematic, allowed}) =>
+    Schematic({
+      schematic,
+      allowed: Array.map(allowed, i =>
+        if i >= from {
+          i + amount
+        } else {
+          i
+        }
+      ),
+    })
+  }
+let place = (x: int, ~scope: array<string>) => Schematic({
+  schematic: x,
+  allowed: Array.fromInitializer(~length=Array.length(scope), i => i),
+})
 type gen = ref<int>
-let seen = (g : gen, s : int) => {
-  if (s >= g.contents) { 
+let seen = (g: gen, s: int) => {
+  if s >= g.contents {
     g := s + 1
   }
 }
-let fresh = (g : gen, ~replacing as _ =?) => {
+let fresh = (g: gen, ~replacing as _=?) => {
   let v = g.contents
   g := g.contents + 1
   v
 }
-let prettyPrintVar = (idx: int, scope: array<string>) => switch scope[idx] {
-| Some(n) if Array.indexOf(scope,n) == idx && false => n
-| _ => "\\"->String.concat(String.make(idx))
-}
+let prettyPrintVar = (idx: int, scope: array<string>) =>
+  switch scope[idx] {
+  | Some(n) if Array.indexOf(scope, n) == idx && false => n
+  | _ => "\\"->String.concat(String.make(idx))
+  }
 let makeGen = () => {
   ref(0)
 }
-let rec prettyPrint = (it: t, ~scope: array<string>) => switch it{
-| Symbol({name}) => name
-| Var({idx}) => prettyPrintVar(idx,scope)
-| Schematic({schematic,allowed}) => 
-  "?"->String.concat(String.make(schematic))
+let rec prettyPrint = (it: t, ~scope: array<string>) =>
+  switch it {
+  | Symbol({name}) => name
+  | Var({idx}) => prettyPrintVar(idx, scope)
+  | Schematic({schematic, allowed}) =>
+    "?"
+    ->String.concat(String.make(schematic))
     ->String.concat("(")
-    ->String.concat(Array.join(allowed->Array.map(idx =>prettyPrintVar(idx,scope))," "))
+    ->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " "))
     ->String.concat(")")
-| Compound({subexps}) =>
-  "("->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e,~scope=scope)), " "))
+  | Compound({subexps}) =>
+    "("
+    ->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " "))
     ->String.concat(")")
-}
-let symbolRegexpString = "^([^\\s()]+)";
-let varRegexpString = "^\\\\([0-9]+)$";
-let schematicRegexpString = "^\\?([0-9]+)$";
+  }
+let symbolRegexpString = "^([^\\s()]+)"
+let varRegexpString = "^\\\\([0-9]+)$"
+let schematicRegexpString = "^\\?([0-9]+)$"
 type lexeme = LParen | RParen | VarT(int) | SymbolT(string) | SchematicT(int)
 let nameRES = "^([^\\s.\\[\\]()]+)\\."
 let prettyPrintMeta = (str: string) => {
-  String.concat(str,".")
+  String.concat(str, ".")
 }
 let parseMeta = (str: string) => {
-  let re = RegExp.fromStringWithFlags(nameRES,~flags="y")
+  let re = RegExp.fromStringWithFlags(nameRES, ~flags="y")
   switch re->RegExp.exec(str->String.trim) {
   | None => Error("not a meta name")
-  | Some(res) => switch RegExp.Result.matches(res) {
-    | [n] => Ok(n,String.sliceToEnd(str->String.trim,~start=RegExp.lastIndex(re)))
+  | Some(res) =>
+    switch RegExp.Result.matches(res) {
+    | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re)))
     | _ => Error("impossible happened")
     }
   }
 }
 let parse = (str: string, ~scope: array<string>, ~gen=?) => {
-  let cur = ref(String.make(str));
-  let lex : () => option<lexeme> = () => {
-    let str = String.trim(cur.contents);
+  let cur = ref(String.make(str))
+  let lex: unit => option<lexeme> = () => {
+    let str = String.trim(cur.contents)
     cur := str
     let checkVariable = (candidate: string) => {
       let varRegexp = RegExp.fromString(varRegexpString)
-      switch (Array.indexOf(scope,candidate)) {
-      | -1 => switch varRegexp->RegExp.exec(candidate) {
-        | Some(res') => switch RegExp.Result.matches(res') {
+      switch Array.indexOf(scope, candidate) {
+      | -1 =>
+        switch varRegexp->RegExp.exec(candidate) {
+        | Some(res') =>
+          switch RegExp.Result.matches(res') {
           | [idx] => Some(idx->Int.fromString->Option.getUnsafe)
           | _ => None
           }
@@ -196,26 +231,28 @@ let parse = (str: string, ~scope: array<string>, ~gen=?) => {
       | idx => Some(idx)
       }
     }
-    if (String.get(str,0) == Some("(")) {
-      cur := String.sliceToEnd(str,~start=1)
+    if String.get(str, 0) == Some("(") {
+      cur := String.sliceToEnd(str, ~start=1)
       Some(LParen)
-    } else if (String.get(str,0) == Some(")")) {
-      cur := String.sliceToEnd(str,~start=1)
+    } else if String.get(str, 0) == Some(")") {
+      cur := String.sliceToEnd(str, ~start=1)
       Some(RParen)
     } else {
-      let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString,~flags="y")
+      let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y")
       switch symbolRegexp->RegExp.exec(str) {
       | None => None
-      | Some(res) => switch RegExp.Result.matches(res) {
+      | Some(res) =>
+        switch RegExp.Result.matches(res) {
         | [symb] => {
-            cur := String.sliceToEnd(str,~start=RegExp.lastIndex(symbolRegexp))
+            cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
             switch checkVariable(symb) {
             | Some(idx) => Some(VarT(idx))
             | None => {
                 let schematicRegexp = RegExp.fromString(schematicRegexpString)
                 switch schematicRegexp->RegExp.exec(symb) {
                 | None => Some(SymbolT(symb))
-                | Some(res') => switch RegExp.Result.matches(res') {
+                | Some(res') =>
+                  switch RegExp.Result.matches(res') {
                   | [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe))
                   | _ => Some(SymbolT(symb))
                   }
@@ -228,43 +265,50 @@ let parse = (str: string, ~scope: array<string>, ~gen=?) => {
       }
     }
   }
-  
+
   let peek = () => {
     // a bit slow, better would be to keep a backlog of lexed tokens..
     let str = String.make(cur.contents)
     let tok = lex()
     cur := str
-    tok  
+    tok
   }
   exception ParseError(string)
   let rec parseExp = () => {
     let tok = peek()
     switch tok {
-    | Some(SymbolT(s)) => { let _ = lex(); Some(Symbol({name: s})) }
-    | Some(VarT(idx)) => { let _ = lex(); Some(Var({idx: idx})) }
+    | Some(SymbolT(s)) => {
+        let _ = lex()
+        Some(Symbol({name: s}))
+      }
+    | Some(VarT(idx)) => {
+        let _ = lex()
+        Some(Var({idx: idx}))
+      }
     | Some(SchematicT(num)) => {
-        let _ = lex();
+        let _ = lex()
         switch lex() {
         | Some(LParen) => {
             let it = ref(None)
-            let bits = [];
-            let getVar = (t : option<lexeme>) => switch t {
-            | Some(VarT(idx)) => Some(idx)
-            | _ => None
-            }
-            while {it := lex(); it.contents->getVar->Option.isSome} {
+            let bits = []
+            let getVar = (t: option<lexeme>) =>
+              switch t {
+              | Some(VarT(idx)) => Some(idx)
+              | _ => None
+              }
+            while {
+              it := lex()
+              it.contents->getVar->Option.isSome
+            } {
               Array.push(bits, it.contents->getVar->Option.getUnsafe)
             }
             switch it.contents {
-            | Some(RParen) => {
-                switch gen {
-                | Some(g) => {
-                    seen(g,num);
-                    Some(Schematic({schematic: num, allowed: bits }))
-                  }
-                | None => raise(ParseError("Schematics not allowed here"))
+            | Some(RParen) => switch gen {
+              | Some(g) => {
+                  seen(g, num)
+                  Some(Schematic({schematic: num, allowed: bits}))
                 }
-                
+              | None => raise(ParseError("Schematics not allowed here"))
               }
             | _ => raise(ParseError("Expected closing parenthesis"))
             }
@@ -273,14 +317,17 @@ let parse = (str: string, ~scope: array<string>, ~gen=?) => {
         }
       }
     | Some(LParen) => {
-        let _ = lex();
-        let bits = [];
+        let _ = lex()
+        let bits = []
         let it = ref(None)
-        while {it := parseExp(); it.contents->Option.isSome} {
+        while {
+          it := parseExp()
+          it.contents->Option.isSome
+        } {
           Array.push(bits, it.contents->Option.getUnsafe)
         }
         switch lex() {
-        | Some(RParen) => Some(Compound({subexps:bits}))
+        | Some(RParen) => Some(Compound({subexps: bits}))
         | _ => raise(ParseError("Expected closing parenthesis"))
         }
       }
@@ -290,7 +337,6 @@ let parse = (str: string, ~scope: array<string>, ~gen=?) => {
   switch parseExp() {
   | exception ParseError(s) => Error(s)
   | None => Error("No expression to parse")
-  | Some(e) => Ok((e,cur.contents)) 
+  | Some(e) => Ok((e, cur.contents))
   }
 }
-
diff --git a/src/SExp.resi b/src/SExp.resi
index de8f044..eacc754 100644
--- a/src/SExp.resi
+++ b/src/SExp.resi
@@ -1,12 +1,11 @@
-
 type rec t =
-    Symbol({name: string }) 
-  | Compound({subexps: array<t>}) 
-  | Var({idx:int}) 
-  | Schematic({schematic:int, allowed: array<int>})
+  | Symbol({name: string})
+  | Compound({subexps: array<t>})
+  | Var({idx: int})
+  | Schematic({schematic: int, allowed: array<int>})
 
-include Signatures.TERM with 
-  type t := t and
-  type meta = string and
-  type schematic = int and
-  type subst = Map.t<int,t>
\ No newline at end of file
+include Signatures.TERM
+  with type t := t
+  and type meta = string
+  and type schematic = int
+  and type subst = Map.t<int, t>
diff --git a/src/SExpJView.res b/src/SExpJView.res
index 51ed7c8..f034f66 100644
--- a/src/SExpJView.res
+++ b/src/SExpJView.res
@@ -1,6 +1,6 @@
 module TermView = SExpView
-type props =  {
-  judgment: SExp.t, 
-  scope: array<string>
+type props = {
+  judgment: SExp.t,
+  scope: array<string>,
 }
-let make = ({judgment,scope}) => SExpView.make({term: judgment,scope})
+let make = ({judgment, scope}) => SExpView.make({term: judgment, scope})
diff --git a/src/SExpJView.resi b/src/SExpJView.resi
index 5599070..2077555 100644
--- a/src/SExpJView.resi
+++ b/src/SExpJView.resi
@@ -1 +1 @@
- include Signatures.JUDGMENT_VIEW with module Term := SExp and module Judgment := SExp
\ No newline at end of file
+include Signatures.JUDGMENT_VIEW with module Term := SExp and module Judgment := SExp
diff --git a/src/SExpView.res b/src/SExpView.res
index e1e0e8f..efe6469 100644
--- a/src/SExpView.res
+++ b/src/SExpView.res
@@ -1,55 +1,61 @@
 type props = {term: SExp.t, scope: array<string>}
 open Util
-type idx_props = {idx:int, scope:array<string>}
-let viewVar = (props : idx_props) => switch props.scope[props.idx] {
-| Some(n) if Array.indexOf(props.scope,n) == props.idx => 
-  <span className="term-metavar">
-    { React.string(n)}
-  </span>
-| _ => 
-  <span className="term-metavar-unnamed">
-    {React.string("\\")} { React.int(props.idx) }
-  </span>
-}
+type idx_props = {idx: int, scope: array<string>}
+let viewVar = (props: idx_props) =>
+  switch props.scope[props.idx] {
+  | Some(n) if Array.indexOf(props.scope, n) == props.idx =>
+    <span className="term-metavar"> {React.string(n)} </span>
+  | _ =>
+    <span className="term-metavar-unnamed">
+      {React.string("\\")}
+      {React.int(props.idx)}
+    </span>
+  }
 
-let makeMeta = (str : string) =>
+let makeMeta = (str: string) =>
   <span className="rule-binder">
-    {React.string(str)}{React.string(".")}
+    {React.string(str)}
+    {React.string(".")}
   </span>
 
-let parenthesise = (f) => [
-  <span className="symbol" key={"-1"}>
-    {React.string("(")}
-  </span>,
-  ...f,
-  <span className="symbol" key={"-2"}>
-    {React.string(")")}
-  </span>
-]
-    
-let intersperse = (a) => 
-  a->Array.flatMapWithIndex((e, i) => if i == 0 { [e] } else { [React.string(" "),e] })
-  
+let parenthesise = f =>
+  [
+    <span className="symbol" key={"-1"}> {React.string("(")} </span>,
+    ...f,
+    <span className="symbol" key={"-2"}> {React.string(")")} </span>,
+  ]
+
+let intersperse = a =>
+  a->Array.flatMapWithIndex((e, i) =>
+    if i == 0 {
+      [e]
+    } else {
+      [React.string(" "), e]
+    }
+  )
 
 @react.componentWithProps
-let rec make = ({term, scope}) => switch term {
-| Compound({subexps:bits}) => {
-    <span className="term-compound">
-    {bits
-      ->Array.mapWithIndex( (t, i) => 
-        React.createElement(make,withKey({term:t,scope },i)))
-      ->intersperse->parenthesise->React.array} 
+let rec make = ({term, scope}) =>
+  switch term {
+  | Compound({subexps: bits}) => <span className="term-compound">
+      {bits
+      ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i)))
+      ->intersperse
+      ->parenthesise
+      ->React.array}
     </span>
-    }
-| Var({idx:idx}) => viewVar({idx,scope})
-| Symbol({name:s}) => <span className="term-const"> { React.string(s) } </span>
-| Schematic({schematic:s, allowed:vs}) => 
+  | Var({idx}) => viewVar({idx, scope})
+  | Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span>
+  | Schematic({schematic: s, allowed: vs}) =>
     <span className="term-schematic">
-      {React.string("?")} {React.int(s)} 
+      {React.string("?")}
+      {React.int(s)}
       <span className="term-schematic-telescope">
         {vs
-          ->Array.mapWithIndex( (v,i) => React.createElement(viewVar, withKey({idx:v,scope},i)))
-          ->intersperse->parenthesise->React.array}
+        ->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i)))
+        ->intersperse
+        ->parenthesise
+        ->React.array}
       </span>
     </span>
-}
+  }
diff --git a/src/SExpView.resi b/src/SExpView.resi
index e5b7207..a9cba10 100644
--- a/src/SExpView.resi
+++ b/src/SExpView.resi
@@ -1 +1 @@
-include Signatures.TERM_VIEW with module Term := SExp
\ No newline at end of file
+include Signatures.TERM_VIEW with module Term := SExp
diff --git a/src/ScopeView.res b/src/ScopeView.res
index 0199447..77168a8 100644
--- a/src/ScopeView.res
+++ b/src/ScopeView.res
@@ -1,23 +1,18 @@
 open Signatures
 
-module Make = (
-  Term : TERM,
-  TermView : TERM_VIEW with module Term := Term
-) => {
-  type props = { scope: array<Term.meta> }
+module Make = (Term: TERM, TermView: TERM_VIEW with module Term := Term) => {
+  type props = {scope: array<Term.meta>}
   @react.componentWithProps
-  let make = (props) => {
-    let arr = props.scope->Array.mapWithIndex((m,i) =>
-      <React.Fragment key={String.make(i)}>
-        {TermView.makeMeta(m)}
-      </React.Fragment>)
+  let make = props => {
+    let arr =
+      props.scope->Array.mapWithIndex((m, i) =>
+        <React.Fragment key={String.make(i)}> {TermView.makeMeta(m)} </React.Fragment>
+      )
     Array.reverse(arr)
-    if Array.length(arr) > 0 { 
-      <span className="rule-binders">
-        {React.array(arr)}
-      </span> 
+    if Array.length(arr) > 0 {
+      <span className="rule-binders"> {React.array(arr)} </span>
     } else {
       React.null
     }
   }
-}
\ No newline at end of file
+}
diff --git a/src/Scratch.res b/src/Scratch.res
index e0b3cfb..0596431 100644
--- a/src/Scratch.res
+++ b/src/Scratch.res
@@ -1,5 +1,9 @@
-module AxiomS = Editable.TextArea(AxiomSet.Make(SExp,SExp,SExpJView))
-module DerivationsOrLemmasView = MethodView.CombineMethodView(SExp,SExp,MethodView.DerivationView(SExp,SExp),MethodView.LemmaView(SExp,SExp,SExpJView))
-module TheoremS = Editable.TextArea(Theorem.Make(SExp,SExp,SExpJView,DerivationsOrLemmasView))
-module ConfS = ConfigBlock.Make(SExp,SExp)
-
+module AxiomS = Editable.TextArea(AxiomSet.Make(SExp, SExp, SExpJView))
+module DerivationsOrLemmasView = MethodView.CombineMethodView(
+  SExp,
+  SExp,
+  MethodView.DerivationView(SExp, SExp),
+  MethodView.LemmaView(SExp, SExp, SExpJView),
+)
+module TheoremS = Editable.TextArea(Theorem.Make(SExp, SExp, SExpJView, DerivationsOrLemmasView))
+module ConfS = ConfigBlock.Make(SExp, SExp)
diff --git a/src/Signatures.res b/src/Signatures.res
index 9dd3ae2..2a9034d 100644
--- a/src/Signatures.res
+++ b/src/Signatures.res
@@ -1,52 +1,48 @@
-
 module type TERM = {
   type t
   type schematic
   type meta
-  type subst = Map.t<schematic,t>
-  let substitute : (t, subst) => t
-  let unify : (t, t) => array<subst>
+  type subst = Map.t<schematic, t>
+  let substitute: (t, subst) => t
+  let unify: (t, t) => array<subst>
   // law: unify(a,b) == [{}] iff equivalent(a,b)
-  let equivalent : (t, t) => bool
-  let substDeBruijn  : (t, array<t>, ~from:int=?) => t
-  let upshift : (t, int, ~from:int=?) => t    
+  let equivalent: (t, t) => bool
+  let substDeBruijn: (t, array<t>, ~from: int=?) => t
+  let upshift: (t, int, ~from: int=?) => t
   type gen
-  let fresh : (gen, ~replacing:meta=?) => schematic
-  let seen : (gen, schematic) => ()
-  let place : (schematic, ~scope: array<meta>) => t
-  let makeGen : () => gen
-  let parse : (string, ~scope: array<meta>, ~gen: gen=?) => result<(t,string),string>
-  let parseMeta : (string) => result<(meta,string),string>
-  let prettyPrint : (t, ~scope: array<meta>) => string
-  let prettyPrintMeta : (meta) => string
+  let fresh: (gen, ~replacing: meta=?) => schematic
+  let seen: (gen, schematic) => unit
+  let place: (schematic, ~scope: array<meta>) => t
+  let makeGen: unit => gen
+  let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, string), string>
+  let parseMeta: string => result<(meta, string), string>
+  let prettyPrint: (t, ~scope: array<meta>) => string
+  let prettyPrintMeta: meta => string
 }
 
 module type JUDGMENT = {
-  module Term : TERM
+  module Term: TERM
   type t
-  let substitute : (t, Term.subst) => t
-  let equivalent : (t,t) => bool
-  let unify : (t, t) => array<Term.subst>
-  let substDeBruijn  : (t, array<Term.t>, ~from:int=?) => t
-  let upshift : (t, int, ~from:int=?) => t
-  let parse : (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t,string),string>
-  let prettyPrint : (t, ~scope: array<Term.meta>) => string
+  let substitute: (t, Term.subst) => t
+  let equivalent: (t, t) => bool
+  let unify: (t, t) => array<Term.subst>
+  let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t
+  let upshift: (t, int, ~from: int=?) => t
+  let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
+  let prettyPrint: (t, ~scope: array<Term.meta>) => string
 }
 
-
 module type TERM_VIEW = {
-  module Term : TERM
+  module Term: TERM
   type props = {term: Term.t, scope: array<Term.meta>}
-  let make : props => React.element
-  let makeMeta : Term.meta => React.element
+  let make: props => React.element
+  let makeMeta: Term.meta => React.element
 }
 
 module type JUDGMENT_VIEW = {
-  module Term : TERM
-  module Judgment : JUDGMENT with module Term := Term;
-  module TermView : TERM_VIEW with module Term := Term;
+  module Term: TERM
+  module Judgment: JUDGMENT with module Term := Term
+  module TermView: TERM_VIEW with module Term := Term
   type props = {judgment: Judgment.t, scope: array<Term.meta>}
-  let make : props => React.element
-} 
-
-
+  let make: props => React.element
+}
diff --git a/src/Theorem.res b/src/Theorem.res
index 736ec8a..4089c07 100644
--- a/src/Theorem.res
+++ b/src/Theorem.res
@@ -2,60 +2,65 @@ open Signatures
 open Component
 open MethodView
 module Make = (
-  Term : TERM, 
-  Judgment : JUDGMENT with module Term := Term,
-  JudgmentView : JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
-  MethodView : METHOD_VIEW with module Term := Term and module Judgment := Judgment
+  Term: TERM,
+  Judgment: JUDGMENT with module Term := Term,
+  JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,
+  MethodView: METHOD_VIEW with module Term := Term and module Judgment := Judgment,
 ) => {
-  module Rule = Rule.Make(Term,Judgment)
-  module Proof = Proof.Make(Term,Judgment,MethodView.Method)
-  module Context = Method.Context(Term,Judgment)
-  module ProofView = ProofView.Make(Term,Judgment,JudgmentView,MethodView)
+  module Rule = Rule.Make(Term, Judgment)
+  module Proof = Proof.Make(Term, Judgment, MethodView.Method)
+  module Context = Method.Context(Term, Judgment)
+  module ProofView = ProofView.Make(Term, Judgment, JudgmentView, MethodView)
   open RuleView
-  module RuleView = RuleView.Make(Term,Judgment,JudgmentView)
-  module Ports = Ports(Term,Judgment)
-  type props = { content: string, imports: Ports.t, onLoad: (~exports:Ports.t,~string:string=?) => (), onChange: (string,~exports:Ports.t) => () }
+  module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
+  module Ports = Ports(Term, Judgment)
+  type props = {
+    content: string,
+    imports: Ports.t,
+    onLoad: (~exports: Ports.t, ~string: string=?) => unit,
+    onChange: (string, ~exports: Ports.t) => unit,
+  }
   type state = {name: string, rule: Rule.t, proof: Proof.checked}
-  let deserialise = (facts : Dict.t<Rule.t>, gen : Term.gen, str : string) : result<state,string> => {
+  let deserialise = (facts: Dict.t<Rule.t>, gen: Term.gen, str: string): result<state, string> => {
     let cur = ref(str)
-    switch Rule.parseTopLevel(cur.contents,~scope=[],~gen=gen) {
+    switch Rule.parseTopLevel(cur.contents, ~scope=[], ~gen) {
     | Error(e) => Error(e)
-    | Ok(((r,n),s)) => switch Proof.parse(s,~scope=[],~gen=gen) {
+    | Ok(((r, n), s)) =>
+      switch Proof.parse(s, ~scope=[], ~gen) {
       | Error(e) => Error(e)
-      | Ok((_,s')) if String.length(String.trim(s')) > 0 =>
-          Error("Trailing input: "->String.concat(s'))
-      | Ok((prf,_)) => {
-          let ctx : Context.t = {fixes:[],facts}
-          Ok({name:n,rule:r,proof:Proof.check(ctx,prf,r)})
+      | Ok((_, s')) if String.length(String.trim(s')) > 0 =>
+        Error("Trailing input: "->String.concat(s'))
+      | Ok((prf, _)) => {
+          let ctx: Context.t = {fixes: [], facts}
+          Ok({name: n, rule: r, proof: Proof.check(ctx, prf, r)})
         }
       }
     }
   }
-  let make = (props) => {
-    
+  let make = props => {
     let gen = Term.makeGen()
     switch deserialise(props.imports.facts, gen, props.content) {
     | Ok(state) => {
         React.useEffect(() => {
-          let export = Dict.fromArray([(state.name,state.rule)])
-          props.onLoad(~exports= {Ports.facts: export, ruleStyle: None});
+          let export = Dict.fromArray([(state.name, state.rule)])
+          props.onLoad(~exports={Ports.facts: export, ruleStyle: None})
           None
         }, [])
         let ruleStyle = props.imports.ruleStyle->Option.getOr(Hybrid)
         <>
-        <RuleView rule={state.rule} scope={[]} style={ruleStyle}>
-          {React.string(state.name)} 
-        </RuleView>
-        <ProofView ruleStyle={ruleStyle} scope={[]} proof=state.proof />
+          <RuleView rule={state.rule} scope={[]} style={ruleStyle}>
+            {React.string(state.name)}
+          </RuleView>
+          <ProofView ruleStyle={ruleStyle} scope={[]} proof=state.proof />
         </>
       }
     | Error(err) => {
         React.useEffect(() => {
-          props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None});
+          props.onLoad(~exports={Ports.facts: Dict.make(), ruleStyle: None})
           None
         }, [])
         <div className="error"> {React.string(err)} </div>
-      } 
+      }
     }
   }
 }
diff --git a/src/Util.res b/src/Util.res
index 1052459..10cee30 100644
--- a/src/Util.res
+++ b/src/Util.res
@@ -1,13 +1,13 @@
 let newline = "\n"
-let mapMapValues = (m: Map.t<'a,'b>, f: 'b => 'c) => {
-  let nu = Map.make();
-  m->Map.forEachWithKey((v,k) => {
-    nu->Map.set(k,f(v))
+let mapMapValues = (m: Map.t<'a, 'b>, f: 'b => 'c) => {
+  let nu = Map.make()
+  m->Map.forEachWithKey((v, k) => {
+    nu->Map.set(k, f(v))
   })
   nu
 }
-let withKey: ('props, int) => 'props = %raw(`(props, key) => ({...props, key})`) 
+let withKey: ('props, int) => 'props = %raw(`(props, key) => ({...props, key})`)
 
-let arrayWithIndex = (arr : array<React.element>) => {
-  React.array(arr->Array.mapWithIndex((m,i) => <span key={String.make(i)}>m</span>))
+let arrayWithIndex = (arr: array<React.element>) => {
+  React.array(arr->Array.mapWithIndex((m, i) => <span key={String.make(i)}> m </span>))
 }