sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
definitions))
(pp_term term)
- | CicAst.Ident (name, Some [])
- | CicAst.Ident (name, None) ->
+ | CicAst.Ident (name, Some []) | CicAst.Ident (name, None)
+ | CicAst.Uri (name, Some []) | CicAst.Uri (name, None) ->
name
- | CicAst.Ident (name, Some substs) -> sprintf "%s \\subst [%s]" name (pp_substs substs)
+ | CicAst.Ident (name, Some substs)
+ | CicAst.Uri (name, Some substs) ->
+ sprintf "%s \\subst [%s]" name (pp_substs substs)
| CicAst.Implicit -> "?"
| CicAst.Meta (index, substs) ->
sprintf "%d[%s]" index