Add the possibility to make request on instances #6

nicolas.meric · 2021-12-13T16:07:09Z

nicolas.meric commented

2021-12-13 16:07:09 +00:00

Hello. Here is a new pull request which adds the possibility to make request on instances.
The commit log:

Add a new Term Annotation Antiquotation (TA)
to allow requests on instances.
Example:
@{C-instances} will return all the instances of the class "C"
defined in the generated theory
Update ISA_transformers elaborate function signature to
take into account the case where the term argument
of a TA is irrelevant, for example when a TA has no argument.
Example with the TA of the instances of a class:
@{A-instances}
Here the TA has no argument and none second level type checking is
wished, so its associated check function can be the identity function
with respect to the ISA_transformers chek function type.
Add some request examples in Evaluation.thy
Fix typos

Hello. Here is a new pull request which adds the possibility to make request on instances. The commit log: - Add a new Term Annotation Antiquotation (TA) to allow requests on instances. Example: @{C-instances} will return all the instances of the class "C" defined in the generated theory - Update ISA_transformers elaborate function signature to take into account the case where the term argument of a TA is irrelevant, for example when a TA has no argument. Example with the TA of the instances of a class: @{A-instances} Here the TA has no argument and none second level type checking is wished, so its associated check function can be the identity function with respect to the ISA_transformers chek function type. - Add some request examples in Evaluation.thy - Fix typos

nicolas.meric added 1 commit 2021-12-13 16:07:12 +00:00

Add the possibility to make request on instances 18c0557d01

- Add a new Term Annotation Antiquotation (TA)
  to allow requests on instances.
  Example:
  @{C-instances} will return all the instances of the class "C"
  defined in the generated theory
- Update ISA_transformers elaborate function signature to
  take into account the case where the term argument
  of a TA is irrelevant, for example when a TA has no argument.
  Example with the TA of the instances of a class:
  @{A-instances}
  Here the TA has no argument and none second level type checking is
  wished, so its associated check function can be the identity function
  with respect to the ISA_transformers chek function type.
- Add some request examples in Evaluation.thy
- Fix typos

nicolas.meric requested review from idir.aitsadoune 2021-12-13 16:07:23 +00:00

nicolas.meric requested review from wolff 2021-12-13 16:07:23 +00:00

nicolas.meric requested review from adbrucker 2021-12-13 16:07:23 +00:00

adbrucker referenced this issue from a commit

2021-12-15 22:25:04 +00:00

Merge pull request 'Add the possibility to make request on instances' (#6) from nicolas.meric/Isabelle_DOF:request-on-instances-first-draft into master

adbrucker merged commit 546b4fbcfe into master

2021-12-15 22:25:05 +00:00

Sign in to join this conversation.

No reviewers

No Label

No Milestone

No Assignees

1 Participants

Notifications

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: Isabelle_DOF/Isabelle_DOF#6