diff options
author | Aleksandar Milicevic <unknown> | 2011-08-21 17:56:11 -0700 |
---|---|---|
committer | Aleksandar Milicevic <unknown> | 2011-08-21 17:56:11 -0700 |
commit | 38d32824f9632b9f27ffabd54312fe8bca337d40 (patch) | |
tree | 8868231a90d17209af951d8cf8a87dc194afc967 /Jennisys/DafnyPrinter.fs | |
parent | 42d5b22e17fd7ef11c875114c38571f4cd518895 (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.fs | 3 |
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
|