Skip to content

change inconsistent usage of idfun#138

Merged
gares merged 1 commit into
math-comp:masterfrom
jzc:idfun-change
Jul 21, 2021
Merged

change inconsistent usage of idfun#138
gares merged 1 commit into
math-comp:masterfrom
jzc:idfun-change

Conversation

@jzc
Copy link
Copy Markdown
Contributor

@jzc jzc commented Jul 21, 2021

In 6.2, there is an inconsistent usage of idfun and id. In the code example, a definition of idfun is given, and shows the result of (idfun nat 3) and (idfun _ 3). The next paragraph instead makes references to id instead of idfun. The next code example does Arguments idfun {A} a., but then the next two lines uses id. The text always referred to id, so I replaced the references to idfun with id.

Copy link
Copy Markdown
Member

@gares gares left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@gares gares merged commit 7521045 into math-comp:master Jul 21, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants