From de5c6a62937a7448c2258ad736eaf8c30ca68e6e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 5 Feb 2004 17:18:25 +0000 Subject: [PATCH] added \to notation for anonymous binders Pi and Lambda --- helm/ocaml/cic_transformations/cicAstPp.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml index b1e658876..ee60c4279 100644 --- a/helm/ocaml/cic_transformations/cicAstPp.ml +++ b/helm/ocaml/cic_transformations/cicAstPp.ml @@ -38,6 +38,11 @@ let rec pp_term = function | 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) -- 2.39.2