If the goal/error view contains several errors, then revealing only applies to the last one.
To reproduce, write \func test (n : Nat) : Nat = Nat => cases n {?} and reveal the implicit argument of = in the first goal. It will show the implicit argument in the last one instead.
If the goal/error view contains several errors, then revealing only applies to the last one. To reproduce, write
\func test (n : Nat) : Nat = Nat => cases n {?}and reveal the implicit argument of=in the first goal. It will show the implicit argument in the last one instead.