(pp_term ~pp_parens:true t3)
| Ast.LetRec (kind, definitions, term) ->
let rec get_guard i = function
- | [] -> (*assert false*) Ast.Implicit
+ | [] -> (*assert false*) Ast.Implicit `JustOne
| [term, _] when i = 1 -> term
| _ :: tl -> get_guard (pred i) tl
in
let map (params, (id,typ), body, i) =
let typ =
match typ with
- None -> Ast.Implicit
+ None -> Ast.Implicit `JustOne
| Some typ -> typ
in
sprintf "%s %s on %s: %s \\def %s"
| Ast.Ident (name, Some substs)
| Ast.Uri (name, Some substs) ->
sprintf "%s \\subst [%s]" name (pp_substs substs)
- | Ast.Implicit -> "?"
+ | Ast.Implicit `Vector -> "?"
+ | Ast.Implicit `JustOne -> "…"
| Ast.Meta (index, substs) ->
sprintf "%d[%s]" index
(String.concat "; "
in
match pp_parens, t with
| false, _
- | true, Ast.Implicit
+ | true, Ast.Implicit _
| true, Ast.Sort _
| true, Ast.Ident (_, Some [])
| true, Ast.Ident (_, None) -> t_pp