diff options
author | Malte Voos <git@mal.tc> | 2024-06-30 15:07:02 +0200 |
---|---|---|
committer | Malte Voos <git@mal.tc> | 2024-06-30 15:07:02 +0200 |
commit | fab70aaf2947ff1369757355fbf11437c6db35ff (patch) | |
tree | db4a00cb43cb4c3833091d5a7cd0423a99fb7f82 /src/pretty/Pretty.ml | |
parent | b34ebf3fe3ecaf292be873d231dd54c80f16ad07 (diff) | |
download | toytt-fab70aaf2947ff1369757355fbf11437c6db35ff.tar.gz toytt-fab70aaf2947ff1369757355fbf11437c6db35ff.zip |
implement syntax for non-dependent function and pair types
Diffstat (limited to 'src/pretty/Pretty.ml')
-rw-r--r-- | src/pretty/Pretty.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml index ba78881..8b7ad1a 100644 --- a/src/pretty/Pretty.ml +++ b/src/pretty/Pretty.ml @@ -67,8 +67,9 @@ struct pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case ) fmt - and pp_arg fmt (name, tp) = - Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp + and pp_arg fmt (name, tp) = match name with + | Some name -> (delimited @@ fun fmt (name, tp) -> Fmt.pf fmt "(@[%s@] : @[%a@])" name pp tp) fmt (name, tp) + | None -> pp fmt tp (* TODO: improve indentation *) and pp fmt = function |