diff --git a/src/main.rs b/src/main.rs
index 40d8b12..5d207d3 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -19,14 +19,14 @@ static CONCRETE: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("def")
 const DEFAULT_COMPLEXITY_LIMIT: usize = 200_000;
 const DEFAULT_STEP_LIMIT: usize = 20_000;
 
-fn main() {
+pub fn main() {
     match do_it() {
         Some(out) => println!("{out}"),
         None => println!("error :("),
     }
 }
 
-fn do_it() -> Option<String> {
+pub fn do_it() -> Option<String> {
     let buf = if let Some(buf) = env::args().nth(1) {
         buf
     } else {
@@ -42,13 +42,13 @@ fn do_it() -> Option<String> {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
-enum Sexp {
+pub enum Sexp {
     Atom(Symbol),
     List(Vec<Sexp>),
 }
 
 impl Sexp {
-    fn nil() -> Self {
+    pub fn nil() -> Self {
         Self::List(Vec::new())
     }
 
@@ -56,7 +56,7 @@ impl Sexp {
     ///
     /// [`Atom`]: Sexp::Atom
     #[must_use]
-    fn is_atom(&self) -> bool {
+    pub fn is_atom(&self) -> bool {
         matches!(self, Self::Atom(..))
     }
 
@@ -64,12 +64,12 @@ impl Sexp {
     ///
     /// [`List`]: Sexp::List
     #[must_use]
-    fn is_list(&self) -> bool {
+    pub fn is_list(&self) -> bool {
         matches!(self, Self::List(..))
     }
 
     #[must_use]
-    fn atom(&self) -> Option<&Symbol> {
+    pub fn atom(&self) -> Option<&Symbol> {
         match self {
             Sexp::Atom(at) => Some(at),
             Sexp::List(_) => None,
@@ -77,7 +77,7 @@ impl Sexp {
     }
 
     #[must_use]
-    fn list(&self) -> Option<&[Sexp]> {
+    pub fn list(&self) -> Option<&[Sexp]> {
         match self {
             Sexp::Atom(_) => None,
             Sexp::List(xs) => Some(&xs),
@@ -85,7 +85,7 @@ impl Sexp {
     }
 
     #[must_use]
-    fn unwrap_atom(&self) -> Symbol {
+    pub fn unwrap_atom(&self) -> Symbol {
         match self {
             Sexp::Atom(sym) => *sym,
             Sexp::List(_) => unreachable!(),
@@ -93,19 +93,19 @@ impl Sexp {
     }
 
     /// Push a sexp to the end of a sexp. Does nothing if the sexp is an atom.
-    fn push(&mut self, item: Self) {
+    pub fn push(&mut self, item: Self) {
         match self {
             Sexp::Atom(_) => (),
             Sexp::List(xs) => xs.push(item),
         }
     }
 
-    fn rw(&self, rule: &Rule) -> Sexp {
+    pub fn rw(&self, rule: &Rule) -> Sexp {
         rw(rule, self)
     }
 
     #[must_use]
-    fn pertinent(&self) -> HashSet<Symbol> {
+    pub fn pertinent(&self) -> HashSet<Symbol> {
         match self {
             Sexp::Atom(sym) => {
                 let mut set = HashSet::with_capacity(1);
@@ -121,7 +121,7 @@ impl Sexp {
         }
     }
 
-    fn concretion_targets(&self) -> HashSet<&Sexp> {
+    pub fn concretion_targets(&self) -> HashSet<&Sexp> {
         match self {
             at @ Sexp::Atom(_) => {
                 let mut out = HashSet::with_capacity(1);
@@ -138,7 +138,7 @@ impl Sexp {
     }
 
     #[must_use]
-    fn contains_sym(&self, sym: Symbol) -> bool {
+    pub fn contains_sym(&self, sym: Symbol) -> bool {
         match self {
             Sexp::Atom(at) => *at == sym,
             Sexp::List(xs) => xs.iter().any(|s| s.contains_sym(sym)),
@@ -146,7 +146,7 @@ impl Sexp {
     }
 
     #[must_use]
-    fn complexity(&self) -> usize {
+    pub fn complexity(&self) -> usize {
         match self {
             Sexp::Atom(_) => 1,
             Sexp::List(xs) => 10 + xs.iter().map(Sexp::complexity).sum::<usize>(),
@@ -154,7 +154,7 @@ impl Sexp {
     }
 
     // #[must_use]
-    // fn apply_lets(&self) -> Sexp {
+    // pub fn apply_lets(&self) -> Sexp {
     //     match self {
     //         Sexp::Atom(_) => self.clone(),
     //         Sexp::List(xs) => match Let::from_sexp(self) {
@@ -165,7 +165,7 @@ impl Sexp {
     // }
 
     #[must_use]
-    fn apply_special_form<'src, F: SpecialForm<'src>>(&'src self) -> Sexp {
+    pub fn apply_special_form<'src, F: SpecialForm<'src>>(&'src self) -> Sexp {
         match self {
             Sexp::Atom(_) => match F::from_sexp(self) {
                 Some(form) => form.eval(),
@@ -189,13 +189,13 @@ impl fmt::Display for Sexp {
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
-enum Token<'src> {
+pub enum Token<'src> {
     LParen,
     RParen,
     Atom(&'src str),
 }
 
-fn lex(src: &str) -> Vec<Token> {
+pub fn lex(src: &str) -> Vec<Token> {
     // maybe a bad idea?
     let mut out = Vec::with_capacity(src.len());
 
@@ -260,7 +260,7 @@ fn lex(src: &str) -> Vec<Token> {
     out
 }
 
-fn at_depth(depth: usize, sexp: &mut Sexp) -> &mut Sexp {
+pub fn at_depth(depth: usize, sexp: &mut Sexp) -> &mut Sexp {
     if depth == 0 {
         sexp
     } else {
@@ -271,7 +271,7 @@ fn at_depth(depth: usize, sexp: &mut Sexp) -> &mut Sexp {
     }
 }
 
-fn parse<'src>(tokens: &'src [Token<'src>]) -> Option<Vec<Sexp>> {
+pub fn parse<'src>(tokens: &'src [Token<'src>]) -> Option<Vec<Sexp>> {
     let mut out = Sexp::nil();
     let mut depth = 0;
 
@@ -301,7 +301,7 @@ fn parse<'src>(tokens: &'src [Token<'src>]) -> Option<Vec<Sexp>> {
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
-enum Rule {
+pub enum Rule {
     Forall {
         vars: Vec<Symbol>,
         lhs: Sexp,
@@ -314,15 +314,15 @@ enum Rule {
 }
 
 impl Rule {
-    fn forall(vars: Vec<Symbol>, lhs: Sexp, rhs: Sexp) -> Rule {
+    pub fn forall(vars: Vec<Symbol>, lhs: Sexp, rhs: Sexp) -> Rule {
         Rule::Forall { vars, lhs, rhs }
     }
 
-    fn concrete(lhs: Sexp, rhs: Sexp) -> Rule {
+    pub fn concrete(lhs: Sexp, rhs: Sexp) -> Rule {
         Rule::Concrete { lhs, rhs }
     }
 
-    fn concrify(&self, sexp: &Sexp) -> Rule {
+    pub fn concrify(&self, sexp: &Sexp) -> Rule {
         match self {
             Rule::Forall { vars, lhs, rhs } => {
                 if vars.is_empty() {
@@ -350,7 +350,7 @@ impl Rule {
         }
     }
 
-    fn concretions(&self, targets: &HashSet<&Sexp>) -> HashSet<Rule> {
+    pub fn concretions(&self, targets: &HashSet<&Sexp>) -> HashSet<Rule> {
         if self.is_concrete() {
             let mut out = HashSet::with_capacity(1);
             out.insert(self.clone());
@@ -374,26 +374,26 @@ impl Rule {
         }
     }
 
-    // fn matches(&self, expr: &Sexp) -> bool {
+    // pub fn matches(&self, expr: &Sexp) -> bool {
     //     could_match(self.vars(), self.lhs(), expr)
     // }
 
     #[must_use]
-    fn lhs(&self) -> &Sexp {
+    pub fn lhs(&self) -> &Sexp {
         match self {
             Rule::Concrete { lhs, .. } | Rule::Forall { lhs, .. } => lhs,
         }
     }
 
     #[must_use]
-    fn rhs(&self) -> &Sexp {
+    pub fn rhs(&self) -> &Sexp {
         match self {
             Rule::Forall { rhs, .. } | Rule::Concrete { rhs, .. } => rhs,
         }
     }
 
     #[must_use]
-    fn vars(&self) -> Option<&Vec<Symbol>> {
+    pub fn vars(&self) -> Option<&Vec<Symbol>> {
         match self {
             Rule::Forall { vars, .. } => Some(vars),
             Rule::Concrete { .. } => None,
@@ -401,7 +401,7 @@ impl Rule {
     }
 
     #[must_use]
-    fn num_vars(&self) -> usize {
+    pub fn num_vars(&self) -> usize {
         match self.vars() {
             Some(xs) => xs.len(),
             None => 0,
@@ -409,7 +409,7 @@ impl Rule {
     }
 
     #[must_use]
-    fn rw(&self, sexp: &Sexp) -> Sexp {
+    pub fn rw(&self, sexp: &Sexp) -> Sexp {
         rw(self, sexp)
     }
 
@@ -417,7 +417,7 @@ impl Rule {
     ///
     /// [`Forall`]: Rule::Forall
     #[must_use]
-    fn is_forall(&self) -> bool {
+    pub fn is_forall(&self) -> bool {
         matches!(self, Self::Forall { .. })
     }
 
@@ -425,11 +425,11 @@ impl Rule {
     ///
     /// [`Concrete`]: Rule::Concrete
     #[must_use]
-    fn is_concrete(&self) -> bool {
+    pub fn is_concrete(&self) -> bool {
         matches!(self, Self::Concrete { .. })
     }
 
-    fn var_replace(from: Symbol, to: &Sexp) -> Rule {
+    pub fn var_replace(from: Symbol, to: &Sexp) -> Rule {
         Rule::Concrete {
             lhs: Sexp::Atom(from),
             rhs: to.clone(),
@@ -437,7 +437,7 @@ impl Rule {
     }
 
     #[must_use]
-    fn concrete_with_matches(&self, matches: &Matches<'_>) -> Rule {
+    pub fn concrete_with_matches(&self, matches: &Matches<'_>) -> Rule {
         match self {
             Rule::Forall { vars, .. } => {
                 let mut out = self.clone();
@@ -471,7 +471,7 @@ impl fmt::Display for Rule {
     }
 }
 
-fn could_match(vars: Option<&[Symbol]>, lhs: &Sexp, expr: &Sexp) -> bool {
+pub fn could_match(vars: Option<&[Symbol]>, lhs: &Sexp, expr: &Sexp) -> bool {
     let is_var = |var: &Symbol| -> bool {
         match vars {
             Some(vars) => vars.contains(var),
@@ -493,7 +493,7 @@ type Matches<'src> = HashMap<Symbol, &'src Sexp>;
 
 // DONE?: there. can. be. at most. one. match.
 // i'm happy that this is faster, but it might be worth going back to the per-variable thing
-fn matches<'src>(vars: &[Symbol], lhs: &Sexp, expr: &'src Sexp) -> Option<Matches<'src>> {
+pub fn matches<'src>(vars: &[Symbol], lhs: &Sexp, expr: &'src Sexp) -> Option<Matches<'src>> {
     match (lhs, expr) {
         (Sexp::Atom(a), Sexp::Atom(b)) => {
             if a == b {
@@ -534,7 +534,7 @@ fn matches<'src>(vars: &[Symbol], lhs: &Sexp, expr: &'src Sexp) -> Option<Matche
     }
 }
 
-fn merge_matches<'src>(
+pub fn merge_matches<'src>(
     vars: &[Symbol],
     a: Matches<'src>,
     b: Matches<'src>,
@@ -559,7 +559,7 @@ fn merge_matches<'src>(
     Some(out)
 }
 
-// fn absorb_matches<'src>(from: Matches<'src>, into: &mut Matches<'src>) {
+// pub fn absorb_matches<'src>(from: Matches<'src>, into: &mut Matches<'src>) {
 //     for (var, matches) in from {
 //         let insert_into = into.entry(var).or_default();
 //         for matc in matches {
@@ -568,7 +568,7 @@ fn merge_matches<'src>(
 //     }
 // }
 
-fn rw(rule: &Rule, sexp: &Sexp) -> Sexp {
+pub fn rw(rule: &Rule, sexp: &Sexp) -> Sexp {
     if rule.lhs() == rule.rhs() {
         return sexp.clone();
     }
@@ -597,8 +597,8 @@ fn rw(rule: &Rule, sexp: &Sexp) -> Sexp {
     }
 }
 
-fn simp(rules: &[Rule], mut expr: Sexp, step_limit: usize, complexity_limit: usize) -> Sexp {
-    for i in 0..step_limit {
+pub fn simp(rules: &[Rule], mut expr: Sexp, step_limit: usize, complexity_limit: usize) -> Sexp {
+    for _ in 0..step_limit {
         expr = expr
             .apply_special_form::<Genslop>()
             .apply_special_form::<Log>()
@@ -619,7 +619,7 @@ fn simp(rules: &[Rule], mut expr: Sexp, step_limit: usize, complexity_limit: usi
     expr
 }
 
-trait SpecialForm<'src>: Sized {
+pub trait SpecialForm<'src>: Sized {
     fn from_sexp(sexp: &'src Sexp) -> Option<Self>;
 
     fn eval(self) -> Sexp;
@@ -692,7 +692,7 @@ static GENSLOP: Lazy<Symbol> = Lazy::new(|| TABLE.lock().unwrap().intern("genslo
 struct Genslop;
 
 impl Genslop {
-    fn gen() -> String {
+    pub fn gen() -> String {
         format!(
             "slop-{}",
             rand::thread_rng()
@@ -743,7 +743,7 @@ impl<'src> SpecialForm<'src> for Log<'src> {
     }
 }
 
-fn make_rule(sexp: &Sexp) -> Option<Rule> {
+pub fn make_rule(sexp: &Sexp) -> Option<Rule> {
     match sexp {
         Sexp::List(xs) => match &xs[..] {
             [Sexp::Atom(forall), Sexp::List(vars), lhs, rhs]
@@ -764,7 +764,7 @@ fn make_rule(sexp: &Sexp) -> Option<Rule> {
     }
 }
 
-fn run_program(src: &str, step_limit: usize, complexity_limit: usize) -> Option<Sexp> {
+pub fn run_program(src: &str, step_limit: usize, complexity_limit: usize) -> Option<Sexp> {
     let mut parsed = parse(&lex(src))?;
 
     let expr = parsed.pop()?;
diff --git a/vec.slimp b/vec.slimp
new file mode 100644
index 0000000..8164270
--- /dev/null
+++ b/vec.slimp
@@ -0,0 +1,22 @@
+(forall (name arg type out f) ((the (Pi name type out) f) (the type arg)) (let name arg (the out (f arg))))
+(forall (in out) (-> in out) (Pi _ in out))
+(forall (var body arg) ((lambda var body) arg) (let var arg body))
+
+(def _ genslop)
+(def succ (the (-> nat nat) 1+))
+(def cons (the (Pi A U (Pi B U (-> A (-> B (Pair A B))))) (lambda _ (lambda _ (lambda a (lambda b (pair a b)))))))
+(def car  (the (Pi A U (Pi B U (-> (Pair A B) A)))        (lambda _ (lambda _ (lambda p (car' p))))))
+(forall (a b) (car' (pair a b)) a)
+
+(def vecnil (the (Pi T U (Vec 0 T)) (lambda _ Vecnil)))
+
+; ordering is bad
+(def veccons
+    (the (Pi len nat (Pi T U (-> T (-> (Vec len T) (Vec (1+ len) T)))))
+        (lambda _ (lambda _ (lambda x (lambda xs (Veccons x xs)))))))
+
+(let sym-nil (vecnil (the U symbol))
+(let our-cons-1 ((veccons (the nat 0)) (the U symbol))
+(let our-cons-2 ((veccons (succ (the nat 0))) (the U symbol))
+((our-cons-2 (the symbol h)) ((our-cons-1 (the symbol i)) sym-nil))
+)))