mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-08-16 03:40:33 +03:00
Merge pull request #411 from developedby/experimental
feat: add u120 numbers to desugared tree
This commit is contained in:
Felipe G
GitHub
commit
f68df12bd2
96
Cargo.lock
generated
96
Cargo.lock
generated
@ -30,9 +30,9 @@ checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
|
||||
|
||||
[[package]]
|
||||
name = "base64"
|
||||
version = "0.13.0"
|
||||
version = "0.13.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "904dfeac50f3cdaba28fc6f57fdcddb75f49ed61346676a78c4ffe55877802fd"
|
||||
checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8"
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
@ -69,9 +69,9 @@ checksum = "ec8a7b6a70fde80372154c65702f00a0f56f3e1c36abbc6c440484be248856db"
|
||||
|
||||
[[package]]
|
||||
name = "cc"
|
||||
version = "1.0.73"
|
||||
version = "1.0.76"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2fff2a6927b3bb87f9595d67196a70493f627687a71d87a0d692242c33f58c11"
|
||||
checksum = "76a284da2e6fe2092f2353e51713435363112dfd60030e22add80be333fb928f"
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
@ -81,9 +81,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "3.2.22"
|
||||
version = "3.2.23"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "86447ad904c7fb335a790c9d7fe3d0d971dc523b8ccd1561a520de9a85302750"
|
||||
checksum = "71655c45cb9845d3270c9d6df84ebe72b4dad3c2ba3f7023ad47c144e4e473a5"
|
||||
dependencies = [
|
||||
"atty",
|
||||
"bitflags",
|
||||
@ -98,13 +98,13 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "4.0.15"
|
||||
version = "4.0.22"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6bf8832993da70a4c6d13c581f4463c2bdda27b9bf1c5498dc4365543abe6d6f"
|
||||
checksum = "91b9970d7505127a162fdaa9b96428d28a479ba78c9ec7550a63a5d9863db682"
|
||||
dependencies = [
|
||||
"atty",
|
||||
"bitflags",
|
||||
"clap_derive 4.0.13",
|
||||
"clap_derive 4.0.21",
|
||||
"clap_lex 0.3.0",
|
||||
"once_cell",
|
||||
"strsim",
|
||||
@ -126,9 +126,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "clap_derive"
|
||||
version = "4.0.13"
|
||||
version = "4.0.21"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c42f169caba89a7d512b5418b09864543eeb4d497416c917d7137863bd2076ad"
|
||||
checksum = "0177313f9f02afc995627906bbd8967e2be069f5261954222dac78290c2b9014"
|
||||
dependencies = [
|
||||
"heck",
|
||||
"proc-macro-error",
|
||||
@ -347,9 +347,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "h2"
|
||||
version = "0.3.14"
|
||||
version = "0.3.15"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5ca32592cf21ac7ccab1825cd87f6c9b3d9022c44d086172ed0966bec8af30be"
|
||||
checksum = "5f9f29bc9dda355256b2916cf526ab02ce0aeaaaf2bad60d65ef3f12f11dd0f4"
|
||||
dependencies = [
|
||||
"bytes",
|
||||
"fnv",
|
||||
@ -431,7 +431,7 @@ version = "0.1.89"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e0581f8e42136b54e77d3180b6c871486ad2a2dca5e394daaa38fa3190dd00c9"
|
||||
dependencies = [
|
||||
"clap 3.2.22",
|
||||
"clap 3.2.23",
|
||||
"highlight_error",
|
||||
"instant",
|
||||
"itertools",
|
||||
@ -444,9 +444,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "hyper"
|
||||
version = "0.14.20"
|
||||
version = "0.14.23"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "02c929dc5c39e335a03c405292728118860721b10190d98c2a0f0efd5baafbac"
|
||||
checksum = "034711faac9d2166cb1baf1a2fb0b60b1f277f8492fd72176c17f3515e1abd3c"
|
||||
dependencies = [
|
||||
"bytes",
|
||||
"futures-channel",
|
||||
@ -553,9 +553,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "ipnet"
|
||||
version = "2.5.0"
|
||||
version = "2.5.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "879d54834c8c76457ef4293a689b2a8c59b076067ad77b15efafbb05f92a592b"
|
||||
checksum = "f88c5561171189e69df9d98bcf18fd5f9558300f7ea7b801eb8a0fd748bd8745"
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
@ -597,7 +597,7 @@ dependencies = [
|
||||
name = "kind-cli"
|
||||
version = "0.3.0"
|
||||
dependencies = [
|
||||
"clap 4.0.15",
|
||||
"clap 4.0.22",
|
||||
"kind-checker",
|
||||
"kind-driver",
|
||||
"kind-report",
|
||||
@ -720,9 +720,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.135"
|
||||
version = "0.2.137"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "68783febc7782c6c5cb401fbda4de5a9898be1762314da0bb2c10ced61f18b0c"
|
||||
checksum = "fc7fcc620a3bff7cdd7a365be3376c97191aeaccc2a603e600951e452615bf89"
|
||||
|
||||
[[package]]
|
||||
name = "linked-hash-map"
|
||||
@ -763,21 +763,21 @@ checksum = "2a60c7ce501c71e03a9c9c0d35b861413ae925bd979cc7a4e30d060069aaac8d"
|
||||
|
||||
[[package]]
|
||||
name = "mio"
|
||||
version = "0.8.4"
|
||||
version = "0.8.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "57ee1c23c7c63b0c9250c339ffdc69255f110b298b901b9f6c82547b7b87caaf"
|
||||
checksum = "e5d732bc30207a6423068df043e3d02e0735b155ad7ce1a6f76fe2baa5b158de"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"log",
|
||||
"wasi",
|
||||
"windows-sys 0.36.1",
|
||||
"windows-sys 0.42.0",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "native-tls"
|
||||
version = "0.2.10"
|
||||
version = "0.2.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fd7e2f3618557f980e0b17e8856252eee3c97fa12c54dff0ca290fb6266ca4a9"
|
||||
checksum = "07226173c32f2926027b63cce4bcd8076c3552846cbe7925f3aaffeac0a3b92e"
|
||||
dependencies = [
|
||||
"lazy_static",
|
||||
"libc",
|
||||
@ -821,9 +821,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "num_cpus"
|
||||
version = "1.13.1"
|
||||
version = "1.14.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1"
|
||||
checksum = "f6058e64324c71e02bc2b150e4f3bc8286db6c83092132ffa3f6b1eab0f9def5"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
@ -831,9 +831,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "once_cell"
|
||||
version = "1.15.0"
|
||||
version = "1.16.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e82dad04139b71a90c080c8463fe0dc7902db5192d939bd0950f074d014339e1"
|
||||
checksum = "86f0b0d4bf799edbc74508c1e8bf170ff5f41238e5f8225603ca7caaae2b7860"
|
||||
|
||||
[[package]]
|
||||
name = "openssl"
|
||||
@ -869,9 +869,9 @@ checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf"
|
||||
|
||||
[[package]]
|
||||
name = "openssl-sys"
|
||||
version = "0.9.76"
|
||||
version = "0.9.77"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5230151e44c0f05157effb743e8d517472843121cf9243e8b81393edb5acd9ce"
|
||||
checksum = "b03b84c3b2d099b81f0953422b4d4ad58761589d0229b5506356afca05a3670a"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"cc",
|
||||
@ -882,9 +882,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "os_str_bytes"
|
||||
version = "6.3.0"
|
||||
version = "6.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9ff7415e9ae3fff1225851df9e0d9e4e5479f947619774677a63572e55e80eff"
|
||||
checksum = "3baf96e39c5359d2eb0dd6ccb42c62b91d9678aa68160d261b9e0ccbf9e9dea9"
|
||||
|
||||
[[package]]
|
||||
name = "parking_lot_core"
|
||||
@ -919,9 +919,9 @@ checksum = "8b870d8c151b6f2fb93e84a13146138f05d02ed11c7e7c54f8826aaaf7c9f184"
|
||||
|
||||
[[package]]
|
||||
name = "pkg-config"
|
||||
version = "0.3.25"
|
||||
version = "0.3.26"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1df8c4ec4b0627e53bdf214615ad287367e482558cf84b109250b37464dc03ae"
|
||||
checksum = "6ac9a59f73473f1b8d852421e59e64809f025994837ef743615c6d0c5b305160"
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro-error"
|
||||
@ -949,9 +949,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.46"
|
||||
version = "1.0.47"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "94e2ef8dbfc347b10c094890f778ee2e36ca9bb4262e86dc99cd217e35f3470b"
|
||||
checksum = "5ea3d908b0e36316caf9e9e2c4625cdde190a7e6f440d794667ed17a1855e725"
|
||||
dependencies = [
|
||||
"unicode-ident",
|
||||
]
|
||||
@ -991,9 +991,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "regex"
|
||||
version = "1.6.0"
|
||||
version = "1.7.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4c4eb3267174b8c6c2f654116623910a0fef09c4753f8dd83db29c48a0df988b"
|
||||
checksum = "e076559ef8e241f2ae3479e36f97bd5741c0330689e217ad51ce2c76808b868a"
|
||||
dependencies = [
|
||||
"aho-corasick",
|
||||
"memchr",
|
||||
@ -1002,9 +1002,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "regex-syntax"
|
||||
version = "0.6.27"
|
||||
version = "0.6.28"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a3f87b73ce11b1619a3c6332f45341e0047173771e8b8b73f87bfeefb7b56244"
|
||||
checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848"
|
||||
|
||||
[[package]]
|
||||
name = "remove_dir_all"
|
||||
@ -1108,9 +1108,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "serde"
|
||||
version = "1.0.145"
|
||||
version = "1.0.147"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "728eb6351430bccb993660dfffc5a72f91ccc1295abaa8ce19b27ebe4f75568b"
|
||||
checksum = "d193d69bae983fc11a79df82342761dfbf28a99fc8d203dca4c3c1b590948965"
|
||||
|
||||
[[package]]
|
||||
name = "serde_json"
|
||||
@ -1178,9 +1178,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.102"
|
||||
version = "1.0.103"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3fcd952facd492f9be3ef0d0b7032a6e442ee9b361d4acc2b1d0c4aaa5f613a1"
|
||||
checksum = "a864042229133ada95abf3b54fdc62ef5ccabe9515b64717bcb9a1919e59445d"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
@ -1212,9 +1212,9 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "textwrap"
|
||||
version = "0.15.1"
|
||||
version = "0.16.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "949517c0cf1bf4ee812e2e07e08ab448e3ae0d23472aee8a06c985f0c8815b16"
|
||||
checksum = "222a222a5bfe1bba4a77b45ec488a741b3cb8872e5e499451fd7d0129c9c7c3d"
|
||||
|
||||
[[package]]
|
||||
name = "tinyvec"
|
||||
|
||||
@ -132,7 +132,8 @@ fn codegen_all_expr(
|
||||
|
||||
match &expr.data {
|
||||
Typ => mk_quoted_ctr(eval_ctr(quote, TermTag::Typ), vec![span_to_num(expr.span)]),
|
||||
U60 => mk_quoted_ctr(eval_ctr(quote, TermTag::U60), vec![span_to_num(expr.span)]),
|
||||
NumType(desugared::NumType::U60) => mk_quoted_ctr(eval_ctr(quote, TermTag::U60), vec![span_to_num(expr.span)]),
|
||||
NumType(desugared::NumType::U120) => todo!(),
|
||||
Var(ident) => {
|
||||
if quote && !lhs {
|
||||
set_origin(ident)
|
||||
@ -240,10 +241,11 @@ fn codegen_all_expr(
|
||||
codegen_all_expr(lhs_rule, lhs, num, quote, expr),
|
||||
],
|
||||
),
|
||||
Num(n) => mk_quoted_ctr(
|
||||
Num(desugared::Num::U60(n)) => mk_quoted_ctr(
|
||||
eval_ctr(quote, TermTag::Num),
|
||||
vec![span_to_num(expr.span), mk_u60(*n)],
|
||||
),
|
||||
Num(desugared::Num::U120(n)) => todo!(),
|
||||
Binary(operator, left, right) => mk_quoted_ctr(
|
||||
eval_ctr(quote, TermTag::Binary),
|
||||
vec![
|
||||
|
||||
@ -149,7 +149,7 @@ fn parse_all_expr(
|
||||
)),
|
||||
"Kind.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
|
||||
"Kind.Quoted.u60" => Ok(Expr::u60(parse_orig(&args[0])?)),
|
||||
"Kind.Quoted.num" => Ok(Expr::num(parse_orig(&args[0])?, parse_num(&args[1])?)),
|
||||
"Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120?
|
||||
"Kind.Quoted.op2" => Ok(Expr::binary(
|
||||
parse_orig(&args[0])?,
|
||||
parse_op(&args[1])?,
|
||||
|
||||
@ -17,7 +17,8 @@ impl<'a> DesugarState<'a> {
|
||||
Literal::Type => desugared::Expr::typ(range),
|
||||
Literal::Help(name) => desugared::Expr::hlp(range, name.clone()),
|
||||
Literal::U60 => desugared::Expr::u60(range),
|
||||
Literal::Number(num) => desugared::Expr::num(range, *num),
|
||||
// TODO: Add u120 literals
|
||||
Literal::Number(num) => desugared::Expr::num60(range, *num),
|
||||
Literal::String(string) => desugared::Expr::str(range, string.to_owned()),
|
||||
Literal::Char(_) => todo!(),
|
||||
}
|
||||
|
||||
@ -304,7 +304,8 @@ impl<'a> DesugarState<'a> {
|
||||
desugared::Expr::var(name)
|
||||
}
|
||||
concrete::pat::PatKind::Var(ident) => desugared::Expr::var(ident.0.clone()),
|
||||
concrete::pat::PatKind::Num(n) => desugared::Expr::num(pat.range, *n),
|
||||
// TODO: Add u120 pattern literals
|
||||
concrete::pat::PatKind::Num(n) => desugared::Expr::num60(pat.range, *n),
|
||||
concrete::pat::PatKind::Pair(fst, snd) => self.desugar_pair_pat(pat.range, fst, snd),
|
||||
concrete::pat::PatKind::List(ls) => self.desugar_list_pat(pat.range, ls),
|
||||
concrete::pat::PatKind::Str(string) => {
|
||||
|
||||
@ -255,7 +255,7 @@ impl<'a> ErasureState<'a> {
|
||||
use kind_tree::desugared::ExprKind::*;
|
||||
|
||||
match &expr.data {
|
||||
Typ | U60 | Num(_) | Str(_) | Err => Box::new(expr.clone()),
|
||||
Typ | NumType(_) | Num(_) | Str(_) | Err => Box::new(expr.clone()),
|
||||
Hole(_) | Hlp(_) => match &expr.span {
|
||||
kind_span::Span::Generated => Box::new(expr.clone()),
|
||||
kind_span::Span::Locatable(span) => {
|
||||
|
||||
@ -30,14 +30,16 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
|
||||
}),
|
||||
Ann(left, _) => compile_term(left),
|
||||
Sub(_, _, _, expr) => compile_term(expr),
|
||||
Num(numb) => Box::new(Term::Num { numb: *numb }),
|
||||
Num(desugared::Num::U60(numb)) => Box::new(Term::Num { numb: *numb }),
|
||||
Num(_) => todo!(),
|
||||
Binary(op, l, r) => Box::new(Term::Ctr {
|
||||
name: op.to_string(),
|
||||
args: vec![compile_term(l), compile_term(r)],
|
||||
}),
|
||||
Hole(_) => unreachable!("Internal Error: 'Hole' cannot be a relevant term"),
|
||||
Typ => unreachable!("Internal Error: 'Typ' cannot be a relevant term"),
|
||||
U60 => unreachable!("Internal Error: 'U60' cannot be a relevant term"),
|
||||
NumType(desugared::NumType::U60) => unreachable!("Internal Error: 'U60' cannot be a relevant term"),
|
||||
NumType(desugared::NumType::U120) => unreachable!("Internal Error: 'U120' cannot be a relevant term"),
|
||||
All(_, _, _) => unreachable!("Internal Error: 'All' cannot be a relevant term"),
|
||||
Str(_) => unreachable!("Internal Error: 'Str' cannot be a relevant term"),
|
||||
Hlp(_) => unreachable!("Internal Error: 'Hlp' cannot be a relevant term"),
|
||||
|
||||
@ -39,10 +39,10 @@ pub enum ExprKind {
|
||||
Sub(Ident, usize, usize, Box<Expr>),
|
||||
/// Type Literal
|
||||
Typ,
|
||||
/// U60 Type
|
||||
U60,
|
||||
/// Number literal
|
||||
Num(u64),
|
||||
/// Primitive numeric types
|
||||
NumType(NumType),
|
||||
/// Primitive numeric values
|
||||
Num(Num),
|
||||
/// Very special constructor :)
|
||||
Str(String),
|
||||
/// Binary operation (e.g. 2 + 3)
|
||||
@ -158,14 +158,28 @@ impl Expr {
|
||||
pub fn u60(range: Range) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
span: Span::Locatable(range),
|
||||
data: ExprKind::U60,
|
||||
data: ExprKind::NumType(NumType::U60),
|
||||
})
|
||||
}
|
||||
|
||||
pub fn num(range: Range, num: u64) -> Box<Expr> {
|
||||
pub fn u120(range: Range) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
span: Span::Locatable(range),
|
||||
data: ExprKind::Num(num),
|
||||
data: ExprKind::NumType(NumType::U120),
|
||||
})
|
||||
}
|
||||
|
||||
pub fn num60(range: Range, num: u64) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
span: Span::Locatable(range),
|
||||
data: ExprKind::Num(Num::U60(num)),
|
||||
})
|
||||
}
|
||||
|
||||
pub fn num120(range: Range, num: u128) -> Box<Expr> {
|
||||
Box::new(Expr {
|
||||
span: Span::Locatable(range),
|
||||
data: ExprKind::Num(Num::U120(num)),
|
||||
})
|
||||
}
|
||||
|
||||
@ -205,6 +219,18 @@ impl Expr {
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub enum Num {
|
||||
U60(u64),
|
||||
U120(u128),
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug, Hash, PartialEq, Eq)]
|
||||
pub enum NumType {
|
||||
U60,
|
||||
U120
|
||||
}
|
||||
|
||||
/// An argument is a 'binding' of a name to a type
|
||||
/// it has some other options like
|
||||
/// eras: that express the erasure of this type when
|
||||
@ -285,9 +311,11 @@ impl Display for Expr {
|
||||
use ExprKind::*;
|
||||
match &self.data {
|
||||
Typ => write!(f, "Type"),
|
||||
U60 => write!(f, "U60"),
|
||||
NumType(self::NumType::U60) => write!(f, "U60"),
|
||||
NumType(self::NumType::U120) => write!(f, "U120"),
|
||||
Str(n) => write!(f, "\"{}\"", n),
|
||||
Num(n) => write!(f, "{}", n),
|
||||
Num(self::Num::U60(n)) => write!(f, "{}", n),
|
||||
Num(self::Num::U120(n)) => write!(f, "{}u120", n),
|
||||
All(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
|
||||
Var(name) => write!(f, "{}", name),
|
||||
Lambda(binder, body) => write!(f, "({} => {})", binder, body),
|
||||
|
||||
Loading…
Reference in New Issue
Block a user