From 8be5328b8771ee560922a0767d64b57268e40968 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 1 Nov 2016 16:50:18 -0400 Subject: Change hlist implicit status --- src/Util/HList.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Util/HList.v') diff --git a/src/Util/HList.v b/src/Util/HList.v index addb0e40d..8013e8b15 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -20,13 +20,13 @@ Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type := end. (* tuple map *) -Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall ts : tuple' A n, hlist' F ts -> tuple' B n +Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall {ts : tuple' A n}, hlist' F ts -> tuple' B n := match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with | 0 => fun ts v => f _ v | S n' => fun ts v => (@mapt' n' A F B f _ (fst v), f _ (snd v)) end. Definition mapt {n A F B} (f : forall x : A, F x -> B) - : forall ts : tuple A n, hlist F ts -> tuple B n + : forall {ts : tuple A n}, hlist F ts -> tuple B n := match n return forall ts : tuple A n, hlist F ts -> tuple B n with | 0 => fun ts v => tt | S n' => @mapt' n' A F B f -- cgit v1.2.3