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.

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

Definable metas #233

Closed
valis opened this issue Jul 9, 2020 · 4 comments · Fixed by #254
Closed

Definable metas #233

valis opened this issue Jul 9, 2020 · 4 comments · Fixed by #254
Assignees
Milestone

Comments

@valis
Copy link
Collaborator

valis commented Jul 9, 2020

It may be convenient to be able define meta definitions in Arend code. For example, if we have a meta time that returns the current time and a meta print that prints its argument to stdout, we can implement a meta that runs some other meta and prints the time it took:

\meta runTimed m =>
  \let | t0 => time
       | result => m
       | t1 => time
  \in run {
    print (t1 - t0),
    result
  }
@valis valis added the api label Jul 9, 2020
@ice1000 ice1000 self-assigned this Jul 27, 2020
@ice1000
Copy link
Contributor

ice1000 commented Jul 28, 2020

Do we need to check termination for definable metas? Do we allow non-terminating definable metas?

@ice1000
Copy link
Contributor

ice1000 commented Jul 28, 2020

Do we even allow recursive definable metas?

@valis
Copy link
Collaborator Author

valis commented Jul 29, 2020

Do we need to check termination for definable metas? Do we allow non-terminating definable metas?

No

Do we even allow recursive definable metas?

Yes

ice1000 added a commit that referenced this issue Jul 29, 2020
ice1000 added a commit that referenced this issue Jul 30, 2020
ice1000 added a commit that referenced this issue Jul 30, 2020
ice1000 added a commit that referenced this issue Jul 30, 2020
ice1000 added a commit that referenced this issue Aug 3, 2020
ice1000 added a commit that referenced this issue Aug 7, 2020
ice1000 added a commit that referenced this issue Aug 7, 2020
ice1000 added a commit that referenced this issue Aug 7, 2020
ice1000 added a commit that referenced this issue Aug 9, 2020
ice1000 added a commit that referenced this issue Aug 9, 2020
ice1000 added a commit that referenced this issue Aug 9, 2020
ice1000 added a commit that referenced this issue Aug 9, 2020
ice1000 added a commit that referenced this issue Aug 10, 2020
ice1000 added a commit that referenced this issue Aug 10, 2020
ice1000 added a commit that referenced this issue Aug 10, 2020
ice1000 added a commit that referenced this issue Aug 10, 2020
ice1000 added a commit that referenced this issue Aug 10, 2020
ice1000 added a commit that referenced this issue Aug 10, 2020
ice1000 added a commit that referenced this issue Aug 11, 2020
ice1000 added a commit that referenced this issue Aug 11, 2020
ice1000 added a commit that referenced this issue Aug 11, 2020
ice1000 added a commit that referenced this issue Aug 11, 2020
ice1000 added a commit that referenced this issue Aug 31, 2020
@ice1000 ice1000 added this to the 1.5 milestone Sep 23, 2020
@ice1000
Copy link
Contributor

ice1000 commented Sep 23, 2020

Fixed by #254

@ice1000 ice1000 closed this as completed Sep 23, 2020
@ice1000 ice1000 linked a pull request Sep 23, 2020 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants