From bec4b138090e87fe92c970ca98010e60707c44f9 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 26 Feb 2014 10:12:50 +0100 Subject: fix compilation on Agda 2.3.0.1 --- FinMap.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index b2db8f4..c8b078c 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -38,7 +38,7 @@ fromAscList [] = empty fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A -fromFunc = tabulate ∘ _∘_ just +fromFunc = tabulate ∘ _∘_ Maybe.just reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A reshape m zero = [] -- cgit v1.2.3