summaryrefslogtreecommitdiff
path: root/Jennisys/DafnyPrinter.fs
diff options
context:
space:
mode:
authorGravatar Aleksandar Milicevic <unknown>2011-08-21 17:56:11 -0700
committerGravatar Aleksandar Milicevic <unknown>2011-08-21 17:56:11 -0700
commit38d32824f9632b9f27ffabd54312fe8bca337d40 (patch)
tree8868231a90d17209af951d8cf8a87dc194afc967 /Jennisys/DafnyPrinter.fs
parent42d5b22e17fd7ef11c875114c38571f4cd518895 (diff)
jennisys: got the List.Get example to work. List.Tail also works. Others should follow soon
Diffstat (limited to 'Jennisys/DafnyPrinter.fs')
-rw-r--r--Jennisys/DafnyPrinter.fs3
1 files changed, 3 insertions, 0 deletions
diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 947a72f2..44fd1d50 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -69,6 +69,9 @@ let rec PrintExpr ctx expr =
sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
| MethodCall(rcv,_,name,aparams) ->
sprintf "%s.%s(%s)" (PrintExpr 0 rcv) name (aparams |> PrintSep ", " (PrintExpr 0))
+ | MethodOutSelect(mth,name) ->
+ // TODO: this can only work if there is only 1 out parameter
+ sprintf "%s" (PrintExpr 0 mth)
let rec PrintConst cst =
match cst with