let pp_binder = function
| `Lambda -> "lambda"
- | `Pi -> "pi"
+ | `Pi -> "Pi"
| `Exists -> "exists"
| `Forall -> "forall"
| CicAst.Appl terms ->
sprintf "(%s)" (String.concat " " (List.map pp_term terms))
+ | CicAst.Binder (`Forall, (Cic.Anonymous, typ), body)
+ | CicAst.Binder (`Pi, (Cic.Anonymous, typ), body) ->
+ sprintf "(%s \\to %s)"
+ (match typ with None -> "?" | Some typ -> pp_term typ)
+ (pp_term body)
| CicAst.Binder (kind, var, body) ->
sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var)
(pp_term body)
sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
definitions))
(pp_term term)
- | CicAst.Ident (name, []) -> name
- | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+ | CicAst.Ident (name, Some []) | CicAst.Ident (name, None)
+ | CicAst.Uri (name, Some []) | CicAst.Uri (name, None) ->
+ name
+ | 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
| CicAst.Sort `CProp -> "CProp"
| CicAst.Symbol (name, _) -> name
-and pp_subst (name, term) = sprintf "%s := %s" name (pp_term term)
+ | CicAst.UserInput -> ""
+
+and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
and pp_substs substs = String.concat "; " (List.map pp_subst substs)
and pp_pattern ((head, vars), term) =
- sprintf "%s -> %s"
+ sprintf "%s \\Rightarrow %s"
(match vars with
| [] -> head
| _ ->