Add the possibility to make request on instances #6

Merged
adbrucker merged 1 commits from nicolas.meric/Isabelle_DOF:request-on-instances-first-draft into master 2021-12-15 22:25:05 +00:00
Collaborator

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
18c0557d01 Add the possibility to make request on instances
- 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 merged commit 546b4fbcfe into master 2021-12-15 22:25:05 +00:00
Sign in to join this conversation.
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
No description provided.