From ab6da37b16193dff017cee4ea335606a4aeec94d Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 20 Jun 2017 14:44:15 +0100 Subject: [PATCH] documented problem with holes --- src/Maps.lagda | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/Maps.lagda b/src/Maps.lagda index e5a2996f..4ee53d49 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -295,8 +295,18 @@ updates. ... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z))) ... | no x≢z | yes y≡z rewrite y≡z = {!!} -- sym (update-eq′ ρ z w) ... | yes x≡z | no y≢z rewrite x≡z = {!!} -- update-eq′ ρ z v - ... | no x≢z | no y≢z = {!!} - -- trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z)) + ... | no x≢z | no y≢z = {!!} -- trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z)) + +{- +Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them? +Why does "λ y₁" appear in the final hole? + +?0 : w ≡ ((ρ , z ↦ w) z | z ≟ z) +?1 : ((ρ , z ↦ v) z | z ≟ z) ≡ v +?2 : (((λ y₁ → (ρ , x ↦ v) y₁ | x ≟ y₁) , y ↦ w) z | no y≢z) ≡ +(((λ y₁ → (ρ , y ↦ w) y₁ | y ≟ y₁) , x ↦ v) z | no x≢z) + +-} \end{code}