/// Finish elaborating the patterns into a case tree.
Finish elaborating the patterns into a case tree.
Finish elaborating the patterns into a case tree .
fn done(
    scrutinees: Vec<(Rc<syntax::Term>, Option<Rc<syntax::Term>>)>,
    params: Vec<(AppMode, Option<String>)>,
    body: Rc<syntax::Term>,
) -> Rc<syntax::Term> {
    use mltt_core::syntax::Item::{Declaration, Definition};
    let mut items = Vec::new();
    for (scrutinee, scrutinee_ty) in scrutinees {
        let doc = DocString::from("");
        let label = Label("_".to_owned());
        if let Some(scrutinee_ty) = scrutinee_ty {
            items.push(Declaration(doc.clone(), label.clone(), scrutinee_ty));
        }
        items.push(Definition(doc, label, scrutinee));
    }
    let body = params
        .into_iter()
        .rev()
        .fold(body, |acc, (app_mode, name_hint)| {
            Rc::from(syntax::Term::FunIntro(app_mode, name_hint, acc))
        });
    if items.is_empty() {
        body
    } else {
        Rc::from(syntax::Term::Let(items, body))
    }
}
fn done ( scrutinees : Vec < ( Rc < syntax :: Term > , Option < Rc < syntax :: Term > > ) > , params : Vec < ( AppMode , Option < String > ) > , body : Rc < syntax :: Term > , ) -> Rc < syntax :: Term > { use mltt_core :: syntax :: Item :: { Declaration , Definition } ; let mut items = Vec :: new ( ) ; for ( scrutinee , scrutinee_ty ) in scrutinees { let doc = DocString :: from ( " " ) ; let label = Label ( " " . to_owned ( ) ) ; if let Some ( scrutinee_ty ) = scrutinee_ty { items . push ( Declaration ( doc . clone ( ) , label . clone ( ) , scrutinee_ty ) ) ; } items . push ( Definition ( doc , label , scrutinee ) ) ; } let body = params . into_iter ( ) . rev ( ) . fold ( body , | acc , ( app_mode , name_hint ) | { Rc :: from ( syntax :: Term :: FunIntro ( app_mode , name_hint , acc ) ) } ) ; if items . is_empty ( ) { body } else { Rc :: from ( syntax :: Term :: Let ( items , body ) ) } }
Finish elaborating the patterns into a case tree.
Finish elaborating the patterns into a case tree .
scrutinees
Vec<(Rc<syntax::Term>, Option<Rc<syntax::Term>>)>
params
Vec<(AppMode, Option<String>)>
body
Rc<syntax::Term>