lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Dot-notation helper abbreviations

Open leodemoura opened this issue 2 years ago • 2 comments

During the ICERM after-party hackton, @digama0 suggested we add helper abbreviations such as

abbrev MVarId.getType (mvarId : MVarId) : MetaM Expr

They are great for discoverability when using dot-notation.

leodemoura avatar Jul 21 '22 21:07 leodemoura

@digama0 Any other functions to rename?

leodemoura avatar Aug 04 '22 01:08 leodemoura

I'm going to be making an in depth pass over everything in the coming weeks, so I'll keep an eye out for dot-notation candidates. But I don't have any suggestions at the moment.

digama0 avatar Aug 04 '22 01:08 digama0

Closing this issue for now. We can open a new issue for adding new helper abbreviations if someone has suggestions.

leodemoura avatar Oct 08 '22 02:10 leodemoura