commit fc022a16a452231f4249669eb8fca85702705888
Author: depsterr <depsterr@protonmail.com>
Date:   Thu Aug 25 20:29:55 2022 +0200

    initial commit?

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..e35d885
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+_build
diff --git a/Eval.ml b/Eval.ml
new file mode 100644
index 0000000..4a12c29
--- /dev/null
+++ b/Eval.ml
@@ -0,0 +1,34 @@
+module V = Value
+module T = Term
+
+let rec index : V.env -> int -> V.value
+  = fun env i ->
+    match env with
+    | []      -> failwith "Can't happen"
+    | x :: xs -> if i < 1 then x else index xs (i-1)
+
+let rec eval : V.env -> t.term -> V.value
+  = fun env tr ->
+    match tr with
+    | Var  i                    -> index env i
+    | Type                      -> V.Type
+    | T0                        -> V.T0
+    | Ind0 (B b, t)             -> failwith "todo"
+    | T1                        -> V.T1
+    | T1tr                      -> V.T1tr
+    | Ind1 (B b, t1 tr)         -> failwith "todo"
+    | TNat                      -> V.TNat
+    | Zero                      -> V.Zero
+    | Suc  n                    -> failwith "todo"
+    | IndN (B b, tz, B B ts, n) -> failwith "todo"
+    | TBool                     -> failwith "todo"
+    | True                      -> failwith "todo"
+    | False                     -> failwith "todo"
+    | IndB (B b, tt, tf, b)     -> failwith "todo"
+    | Pi   (dom, B cod)         -> failwith "todo"
+    | Lam  (B body)             -> failwith "todo"
+    | App  (f, x)               -> failwith "todo"
+    | Sg   (ty, tr)             -> failwith "todo"
+    | Pair (x, y)               -> failwith "todo"
+    | Fst  tr                   -> failwith "todo"
+    | Snd  tr                   -> failwith "todo"
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..1f44228
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# implicitt
+
+A "proof assistant" with holes and implcit arguments. Developed to learn about elaboration, meta variables and OCaml
+
+# TODO
+
+* Id types, lol (oops)
+* evaluation
+* conversion
diff --git a/bin/dune b/bin/dune
new file mode 100644
index 0000000..4f94a6e
--- /dev/null
+++ b/bin/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name implicitt)
+ (name main)
+ (libraries implicitt))
diff --git a/bin/main.ml b/bin/main.ml
new file mode 100644
index 0000000..7bf6048
--- /dev/null
+++ b/bin/main.ml
@@ -0,0 +1 @@
+let () = print_endline "Hello, World!"
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..e486793
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.3)
+
+(name implicitt)
+
+(generate_opam_files true)
+
+(source
+ (uri "https://githug.xyz/depsterr/implcitt"))
+
+(authors "depsterr")
+
+(maintainers "depsterr")
+
+(license ISC)
+
+; (documentation https://url/to/documentation)
+
+(package
+ (name implicitt)
+ (synopsis "A poor proof assitant")
+ (description "A \"proof assistant\" with holes and implcit arguments. Developed to learn about elaboration, meta variables and OCaml.")
+ (depends ocaml dune)
+ (tags
+  (topics "proof assistant")))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
diff --git a/implicitt.opam b/implicitt.opam
new file mode 100644
index 0000000..f318f65
--- /dev/null
+++ b/implicitt.opam
@@ -0,0 +1,29 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "A poor proof assitant"
+description:
+  "A \"proof assistant\" with holes and implcit arguments. Developed to learn about elaboration, meta variables and OCaml."
+maintainer: ["depsterr"]
+authors: ["depsterr"]
+license: "ISC"
+tags: ["topics" "proof assistant"]
+depends: [
+  "ocaml"
+  "dune" {>= "3.3"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "https://githug.xyz/depsterr/implcitt"
diff --git a/lib/Term.ml b/lib/Term.ml
new file mode 100644
index 0000000..27f0789
--- /dev/null
+++ b/lib/Term.ml
@@ -0,0 +1,34 @@
+type var = Ix of int
+
+type 'a binder = B of 'a
+
+type term 
+  = Var  of var
+
+  | Type
+
+  | T0
+  | Ind0 of term binder * term
+
+  | T1
+  | T1tr
+  | Ind1 of term binder * term * term
+
+  | TNat
+  | Zero
+  | Suc  of term
+  | IndN of term binder * term * term binder binder * term
+
+  | TBool
+  | True
+  | False
+  | IndB of term binder * term * term * term
+
+  | Pi   of term * term binder
+  | Lam  of term binder
+  | App  of term * term
+
+  | Sg   of term * term binder
+  | Pair of term * term
+  | Fst  of term
+  | Snd  of term
diff --git a/lib/Value.ml b/lib/Value.ml
new file mode 100644
index 0000000..b808561
--- /dev/null
+++ b/lib/Value.ml
@@ -0,0 +1,34 @@
+module T = Term
+
+type lvl = Lvl of int
+
+type closure = C of env * T.term
+
+and env = value list
+
+and value
+  = Type
+  | T0
+  | T1
+  | T1vl
+  | TNat
+  | Suc   of value
+  | Zero
+  | TBool
+  | True
+  | False
+  | Pi    of value * closure
+  | Lam   of closure
+  | Sg    of value * closure
+  | Pair  of value * value
+  | Stuck of stuck * value (* second arg is type *)
+
+and stuck
+  = Var  of lvl
+  | Ind0 of closure * stuck
+  | Ind1 of closure * value * stuck
+  | IndN of closure * value * closure * stuck
+  | IndB of closure * value * value * stuck
+  | App  of stuck * value * value (* fn; val; type of fn *)
+  | Fst  of stuck
+  | Snd  of stuck
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000..c76f468
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,2 @@
+(library
+ (name implicitt))
diff --git a/test/dune b/test/dune
new file mode 100644
index 0000000..ebe353d
--- /dev/null
+++ b/test/dune
@@ -0,0 +1,2 @@
+(test
+ (name implicitt))
diff --git a/test/implicitt.ml b/test/implicitt.ml
new file mode 100644
index 0000000..e69de29