diff options
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index cc2380d5e..2e9f7b0ad 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -103,25 +103,25 @@ Definition curryT (R T : Type) (n : nat) : Type | S n' => curry'T R T n' end. -Fixpoint uncurry' R {T n} : (tuple' T n -> R) -> curry'T R T n +Fixpoint uncurry' {R T n} : (tuple' T n -> R) -> curry'T R T n := match n return (tuple' T n -> R) -> curry'T R T n with | 0 => fun f x => f x | S n' => fun f => @uncurry' (T -> R) T n' (fun xs x => f (xs, x)) end. -Fixpoint uncurry R {T n} : (tuple T n -> R) -> curryT R T n +Fixpoint uncurry {R T n} : (tuple T n -> R) -> curryT R T n := match n return (tuple T n -> R) -> curryT R T n with | 0 => fun f => f tt | S n' => @uncurry' R T n' end. -Fixpoint curry' R {T n} : curry'T R T n -> (tuple' T n -> R) +Fixpoint curry' {R T n} : curry'T R T n -> (tuple' T n -> R) := match n return curry'T R T n -> (tuple' T n -> R) with | 0 => fun f x => f x | S n' => fun f xs_x => @curry' (T -> R) T n' f (fst xs_x) (snd xs_x) end. -Fixpoint curry R {T n} : curryT R T n -> (tuple T n -> R) +Fixpoint curry {R T n} : curryT R T n -> (tuple T n -> R) := match n return curryT R T n -> (tuple T n -> R) with | 0 => fun r _ => r | S n' => @curry' R T n' |