diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-15 14:05:15 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-15 14:05:15 -0500 |
| commit | ec1b80bc84ef06433081adc53474ed11a51ed234 (patch) | |
| tree | 80e744e2ccc43b610350e75eb395c1aee243f338 /src/Util/Tuple.v | |
| parent | 9e6105ece0d7c71c496752c8025b71732172f5e4 (diff) | |
More universe fixes
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index b97bfbc49..d1e0177f2 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -392,9 +392,9 @@ Local Notation option_bind | None => None end). Definition lift_option {n A} (xs : tuple (option A) n) : option (tuple A n) - := lift_monad (fun T => option T) option_bind (@Some) xs. + := lift_monad (fun T => option T) option_bind (fun T v => @Some T v) xs. Definition push_option {n A} (xs : option (tuple A n)) : tuple (option A) n - := push_monad (fun T => option T) option_bind (@Some) xs. + := push_monad (fun T => option T) option_bind (fun T v => @Some T v) xs. Lemma lift_push_option {n A} (xs : option (tuple A (S n))) : lift_option (push_option xs) = xs. Proof. |