diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2010-10-10 13:07:38 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2010-10-10 13:07:38 -0400 |
| commit | d8bc26c9647d2b45009f6538bc2a69508c983449 (patch) | |
| tree | 1d0f355dec824a81d80e9e838e0cae8845f8e179 /src/elab_print.sml | |
| parent | 975b1f43784dfc1769ec93dd5dd408434791464e (diff) | |
Flex kinds for type-level tuples; ::_ notation
Diffstat (limited to 'src/elab_print.sml')
| -rw-r--r-- | src/elab_print.sml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml index 4fb7ee73..279c7231 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -56,6 +56,16 @@ fun p_kind' par env (k, _) = | KError => string "<ERROR>" | KUnif (_, _, ref (SOME k)) => p_kind' par env k | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">") + | KTupleUnif (_, _, ref (SOME k)) => p_kind' par env k + | KTupleUnif (_, nks, _) => box [string "(", + p_list_sep (box [space, string "*", space]) + (fn (n, k) => box [string (Int.toString n ^ ":"), + space, + p_kind env k]) nks, + space, + string "*", + space, + string "...)"] | KRel n => ((if !debug then string (E.lookupKRel env n ^ "_" ^ Int.toString n) |