diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2013-12-17 08:49:24 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2013-12-17 08:49:24 +0100 |
| commit | 88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907 (patch) | |
| tree | 434e67b2e485bee51268cedef1b417424466f958 /BFF.agda | |
| parent | 066861f9cdde4ded6c5442508bef1a27576c68d7 (diff) | |
| download | bidiragda-88ac52ceabaf2bf4a3f27293a8e04a3daaf8b907.tar.gz | |
refactor to get rid of FinMap without Maybe entirely
The union was the only user of this type and now it uses only partial
mappings. So drop remaining uses of FinMap and make everything work with
FinMapMaybe instead.
Diffstat (limited to 'BFF.agda')
| -rw-r--r-- | BFF.agda | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -35,7 +35,7 @@ module VecBFF (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n)) bff get s v = let s′ = enumerate s t′ = get s′ - g = partialize (fromFunc (denumerate s)) + g = fromFunc (denumerate s) g′ = delete-many t′ g h = assoc t′ v h′ = (flip union g′) <$> h |