lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Leading `!` inhibits auto-completion

Open Kha opened this issue 1 year ago • 0 comments

#check id  -- completes here
#check !id  -- doesn't

4.9.0, commit b0c1112471a3f38859d9738184d21132b7d9cd0c

Kha avatar May 24 '24 08:05 Kha