initial parser implementation
This commit is contained in:
parent
8ec95dfbed
commit
8fa38ca7d3
4 changed files with 348 additions and 3 deletions
src
17
src/term.rs
17
src/term.rs
|
@ -54,6 +54,23 @@ impl TypeTerm {
|
|||
self
|
||||
}
|
||||
|
||||
pub fn repr_as(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
|
||||
match self {
|
||||
TypeTerm::Ladder(rungs) => {
|
||||
rungs.push(t.into());
|
||||
}
|
||||
|
||||
_ => {
|
||||
*self = TypeTerm::Ladder(vec![
|
||||
self.clone(),
|
||||
t.into()
|
||||
])
|
||||
}
|
||||
}
|
||||
|
||||
self
|
||||
}
|
||||
|
||||
pub fn num_arg(&mut self, v: i64) -> &mut Self {
|
||||
self.arg(TypeTerm::Num(v))
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue