nar 0.0.8

Narc, a dependently-typed programming language with dependent pattern matching
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

use std::fmt::{Display, Error, Formatter};

use voile_util::{tags::Plicit, uid::UID};
use Plicit::{Ex as Explicit, Im as Implicit};

use crate::syntax::abs::{Abs, Bind};

impl Display for Abs {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        use Abs::*;
        match self {
            Def(id, _gi) => write!(f, "{}", id.text),
            Var(id, UID(uid)) => write!(f, "{}_{:?}", id.text, uid),
            Meta(id, _mi) => write!(f, "?{}", id.text),
            App(a, args) => {
                write!(f, "({} {}", a, args.head())?;
                for arg in args.tail() {
                    write!(f, " {}", arg)?;
                }
                f.write_str(")")
            }
            Pi(_loc, Bind { licit, ty, .. }, clos) => match licit {
                Explicit => write!(f, "({} -> {})", ty, clos),
                Implicit => write!(f, "({{{}}} -> {})", ty, clos),
            },
            Type(_, l) => write!(f, "set{}", l),
            Cons(id, _gi) => write!(f, "{}", id.text),
            Proj(id, _gi) => write!(f, "{}", id.text),
        }
    }
}