let pp_flavour = function
| `Definition -> "definition"
+ | `MutualDefinition -> assert false
| `Fact -> "fact"
| `Goal -> "goal"
| `Lemma -> "lemma"
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+ sprintf "<<pretty printing of mutual definitions not implemented yet>>"
| Ast.Theorem (flavour, name, typ, body) ->
sprintf "%s %s:\n %s\n%s"
(pp_flavour flavour)