summaryrefslogtreecommitdiff
path: root/FinMap.agda
diff options
context:
space:
mode:
authorHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-26 10:12:50 +0100
committerHelmut Grohne <grohne@cs.uni-bonn.de>2014-02-26 10:12:50 +0100
commitbec4b138090e87fe92c970ca98010e60707c44f9 (patch)
tree53e458ee2c6e548979e5e1dd215e4ad379601986 /FinMap.agda
parent28e7397a76be229ba723e49db51d2bf0b87c5493 (diff)
downloadbidiragda-bec4b138090e87fe92c970ca98010e60707c44f9.tar.gz
fix compilation on Agda 2.3.0.1
Diffstat (limited to 'FinMap.agda')
-rw-r--r--FinMap.agda2
1 files changed, 1 insertions, 1 deletions
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 = []