From cd7e8284c7defdad636ffa7ef87f3e584a7592fb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 1 Apr 2019 16:25:31 -0400 Subject: Add support for Sorts in numeral notations --- doc/changelog/03-notations/09883-numeral-notations-sorts.rst | 4 ++++ doc/sphinx/user-extensions/syntax-extensions.rst | 8 ++++---- 2 files changed, 8 insertions(+), 4 deletions(-) create mode 100644 doc/changelog/03-notations/09883-numeral-notations-sorts.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/09883-numeral-notations-sorts.rst b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst new file mode 100644 index 0000000000..abc5a516ae --- /dev/null +++ b/doc/changelog/03-notations/09883-numeral-notations-sorts.rst @@ -0,0 +1,4 @@ +- Numeral Notations now support sorts in the input to printing + functions (e.g., numeral notations can be defined for terms + containing things like `@cons Set nat nil`). (`#9883 + `_, by Jason Gross). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a28ce600ca..02910e603a 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1442,8 +1442,8 @@ Numeral notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). @@ -1592,8 +1592,8 @@ String notations of the resulting term will be refreshed. Note that only fully-reduced ground terms (terms containing only - function application, constructors, inductive type families, and - primitive integers) will be considered for printing. + function application, constructors, inductive type families, + sorts, and primitive integers) will be considered for printing. .. exn:: Cannot interpret this string as a value of type @type -- cgit v1.2.3