From 02e4d1b254a6b8d78badb6c680b69caf6495310a Mon Sep 17 00:00:00 2001
From: Greg Shuflin <greg.shuflin@protonmail.com>
Date: Sun, 5 Mar 2023 11:24:29 -0800
Subject: [PATCH] Initial commit

---
 .gitignore  |  1 +
 Cargo.lock  |  7 +++++++
 Cargo.toml  |  8 ++++++++
 README.md   |  3 +++
 src/main.rs | 26 ++++++++++++++++++++++++++
 5 files changed, 45 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Cargo.lock
 create mode 100644 Cargo.toml
 create mode 100644 README.md
 create mode 100644 src/main.rs

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ea8c4bf
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/target
diff --git a/Cargo.lock b/Cargo.lock
new file mode 100644
index 0000000..dd6fe09
--- /dev/null
+++ b/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "dependent-types"
+version = "0.1.0"
diff --git a/Cargo.toml b/Cargo.toml
new file mode 100644
index 0000000..99b1b60
--- /dev/null
+++ b/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "dependent-types"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..15578cc
--- /dev/null
+++ b/README.md
@@ -0,0 +1,3 @@
+= Rust dependent type implementation
+
+Implementation of https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 in Rust
diff --git a/src/main.rs b/src/main.rs
new file mode 100644
index 0000000..04189c2
--- /dev/null
+++ b/src/main.rs
@@ -0,0 +1,26 @@
+#[derive(Debug)]
+enum Term {
+    //Lambda
+    // Pi
+    Application(Box<Term>, Box<Term>),
+    Annotation(Box<Term>, Box<Term>),
+    FreeVar(u64),
+    Star,
+    BoxTerm
+}
+
+
+fn print(term: &Term, level: u64) -> String {
+    match term {
+        Term::Application(t1, t2) => "".into(),
+        Term::Annotation(t1, t2) => "".into(),
+        Term::FreeVar(x) => format!("{x}"),
+        Term::Star => format!("*"),
+        Term::BoxTerm => format!("☐"),
+    }
+}
+
+
+fn main() {
+    println!("Hello, world!");
+}