Odd <LocalLeader>d Behavior

[DavidHarrison]

The use of d on keyNotInLeaf' fills in decEq x1 x2 = ?DecEq_rhs_1 in the following code:

data Tree : Type -> Type where
  Node : v -> Tree v -> Tree v -> Tree v
  Leaf : Tree v

Map : Type -> Type -> Type
Map k v = Tree (k,v)

data KeyInMap : DecEq key => key -> Map key value -> Type where
  Here  : DecEq key => (k = k') -> KeyInMap k (Node (k',v) l r)
  Left  : DecEq key => KeyInMap k l -> KeyInMap k (Node v l r)
  Right : DecEq key => KeyInMap k r -> KeyInMap k (Node v l r)

keyNotInLeaf' : DecEq key => (m = Leaf) -> KeyInMap k m -> Void
                    decEq x1 x2 = ?DecEq_rhs_1

Thanks,
David Harrison

[xoltar]

I'm seeing the same issue. This is what happens when hitting d on plus':

data Nat' = Z' | S' Nat'                                                           

%name Nat' j,k                                                                     

plus' : Nat' -> Nat' -> Nat'                                                       
        Nat j k = ?Nat_rhs   

[raichoo]

Should be fixed now.

[srenatus]

Seems so, let's close this?