diff options
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 9d169108..ea34ef3d 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -327,6 +327,9 @@ let doc_typ_lem, doc_atomic_typ_lem = String.concat ", " (List.map string_of_kid bad) ^ " escape into Lem")) end + (* AA: I think the correct thing is likely to filter out + non-integer kinded_id's, then use the above code. *) + | Typ_exist (_,_,Typ_aux(Typ_app(id,[_]),_)) when string_of_id id = "atom_bool" -> string "bool" | Typ_exist _ -> unreachable l __POS__ "Non-integer existentials currently unsupported in Lem" (* TODO *) | Typ_bidir _ -> unreachable l __POS__ "Lem doesn't support bidir types" | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown" |