Skip to content

Commit

Permalink
fix: Make Option be co-variant in its type argument
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
RustanLeino committed Mar 13, 2020
1 parent 97681d4 commit b402073
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/StandardLibrary/StandardLibrary.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ module {:extern "STL"} StandardLibrary {
import opened U = UInt

// TODO: Depend on types defined in dafny-lang/libraries instead
datatype Option<T> = None | Some(get: T)
datatype Option<+T> = None | Some(get: T)
{
function method ToResult(): Result<T> {
match this
Expand Down

0 comments on commit b402073

Please sign in to comment.