Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

add abbreviation #365

Closed
leodemoura opened this issue Dec 4, 2014 · 1 comment
Closed

add abbreviation #365

leodemoura opened this issue Dec 4, 2014 · 1 comment
Assignees

Comments

@leodemoura
Copy link
Member

An abbreviation is a definition that is automatically expanded after elaboration.

@leodemoura leodemoura self-assigned this Dec 4, 2014
@fpvandoorn
Copy link
Contributor

In the case of abbreviation is_hset := is_trunc 0, I'd like that the pretty printer also displays is_hset. It would be nice if you could say for abbreviations whether you want to use it for parsing only or for both parsing and pretty printing, similar to notation.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants