clue.txt

<clayrat> dckc-ho, rewrite doesn't work on case expressions, it's a known old bug
<clayrat> https://github.com/idris-lang/Idris-dev/issues/4001
<clayrat> if you define lookup via `with` then that line in the proof is simply `rewrite decEqSelfIsYes {x=key} in Refl`

lookup.idr

module Notation


lookup' : DecEq k => (key: k) -> (dict: List (k, v)) -> Maybe v
lookup' key [] = Nothing
lookup' key ((k0, v0) :: rest) with (decEq key k0)
  | Yes _ = Just v0
  | No _ = (lookup' key rest)


add_1: DecEq k => (key: k) -> (val: v) -> (dict: List (k, v))
    -> (lookup' key ((key, val) :: dict)) = (Just val)
add_1 key val [] =
  rewrite (decEqSelfIsYes {x=key}) in Refl