Updated shorthand notation.
This commit is contained in:
parent
2577669f5f
commit
40082ac32b
|
@ -17,7 +17,7 @@ older versions might be available on a dedicated branch.
|
||||||
* [hiding_type_variables.thy](hiding_type_variables.thy) provides
|
* [hiding_type_variables.thy](hiding_type_variables.thy) provides
|
||||||
print a setup for defining default type variables of type
|
print a setup for defining default type variables of type
|
||||||
constructors. The default type variables can be hidden in output,
|
constructors. The default type variables can be hidden in output,
|
||||||
e.g., `('a, 'b, 'c) foo` is shown as `_ foo`. This shorthand
|
e.g., `('a, 'b, 'c) foo` is shown as `__ foo`. This shorthand
|
||||||
notation can also be used in input (using a parse translation),
|
notation can also be used in input (using a parse translation),
|
||||||
which (sometimes) helps to focus on the important parts of complex
|
which (sometimes) helps to focus on the important parts of complex
|
||||||
type declarations.
|
type declarations.
|
||||||
|
|
Loading…
Reference in New Issue