]> matita.cs.unibo.it Git - helm.git/commitdiff
added \to notation for anonymous binders Pi and Lambda
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 5 Feb 2004 17:18:25 +0000 (17:18 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 5 Feb 2004 17:18:25 +0000 (17:18 +0000)
helm/ocaml/cic_transformations/cicAstPp.ml

index b1e6588766beeeb2b9b3fa1414cdfb2e06ec5871..ee60c427963aa3a191cd4f06c25451330b2b3c8b 100644 (file)
@@ -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)