diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index 1c6c95cb1274e3fbea88c6a3434b1d06815a73e3..0d9b42aa9f87403461e5045570d4bba00b1d0776 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -431,11 +431,16 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe p"""|@$a |""" } - - - p"""|def ${fd.id}(${fd.params}): ${fd.returnType} = { - |""" - + + if (!fd.tparams.isEmpty) { + p"""|def ${fd.id}[${nary(fd.tparams, ",")}](${fd.params}): ${fd.returnType} = { + |""" + } else { + p"""|def ${fd.id}(${fd.params}): ${fd.returnType} = { + |""" + } + + fd.precondition.foreach { case pre => p"""| require($pre) |"""