From b402073df731534837d95830ce6779d54bbebac3 Mon Sep 17 00:00:00 2001 From: "Leino, Rustan" Date: Fri, 13 Mar 2020 15:16:49 -0700 Subject: [PATCH] fix: Make Option be co-variant in its type argument This makes sense for the type Option and could have been done before. We need it in writing a nice `KeyRepr` function for keyrings (see upcoming PR). --- src/StandardLibrary/StandardLibrary.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/StandardLibrary/StandardLibrary.dfy b/src/StandardLibrary/StandardLibrary.dfy index b67299ac6..d531c23f2 100644 --- a/src/StandardLibrary/StandardLibrary.dfy +++ b/src/StandardLibrary/StandardLibrary.dfy @@ -4,7 +4,7 @@ module {:extern "STL"} StandardLibrary { import opened U = UInt // TODO: Depend on types defined in dafny-lang/libraries instead - datatype Option = None | Some(get: T) + datatype Option<+T> = None | Some(get: T) { function method ToResult(): Result { match this