Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Doc comment on data TDef is rejected by the parser #7

Closed
epost opened this issue May 17, 2018 · 1 comment
Closed

Doc comment on data TDef is rejected by the parser #7

epost opened this issue May 17, 2018 · 1 comment
Labels
feature:documentation Issues related to documentation

Comments

@epost
Copy link
Member

epost commented May 17, 2018 •
edited
Loading

https://github.com/typedefs/typedefs/blob/master/src/Typedefs.idr#L13

It says -- ||| now but it ought to be |||; not sure why this is happening, or if this still happens for Idris 1.3.
@tg-x
Copy link
Member

tg-x commented Sep 12, 2018

The doc comment needs to start with a summary, only after that can the arguments be documented.

@epost epost closed this as completed in af78d31 Sep 12, 2018
epost added a commit that referenced this issue Sep 12, 2018
@epost
Merge pull request #41 from typedefs/doc-comment-fix
966cd07 
doc comment fix; resolves #7
@epost epost added the feature:documentation Issues related to documentation label Dec 18, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature:documentation Issues related to documentation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@tg-x @epost