Initial commit
This commit is contained in:
commit
02e4d1b254
|
@ -0,0 +1 @@
|
||||||
|
/target
|
|
@ -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"
|
|
@ -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]
|
|
@ -0,0 +1,3 @@
|
||||||
|
= Rust dependent type implementation
|
||||||
|
|
||||||
|
Implementation of https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196 in Rust
|
|
@ -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!");
|
||||||
|
}
|
Loading…
Reference in New Issue