From 61fd4f06f10bfc62f7aa73ab7f4576600d7692aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Oct 2016 14:54:36 -0400 Subject: Fix implicit status of curry --- src/Util/Tuple.v | 8 ++++---- 1 file 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' -- cgit v1.2.3