"Split atomic pattern" for let expressions

[marat-rkh]

\func lemma1 => (1, 2)
\func lemma2 : Nat => 
  \let p => lemma1 
  \in {?}

"Split atomic pattern" could be suggested for p here.

[ice1000]

So it's gonna be only available when the pattern is irrefutable?

[marat-rkh]

Yes, I think so.