Closed DavidHarrison closed 8 years ago
I'm seeing the same issue. This is what happens when hitting
data Nat' = Z' | S' Nat'
%name Nat' j,k
plus' : Nat' -> Nat' -> Nat'
Nat j k = ?Nat_rhs
Should be fixed now.
The use ofd on
keyNotInLeaf'
fills indecEq x1 x2 = ?DecEq_rhs_1
in the following code:Thanks, David Harrison