clean-up-isa-check-functions #7

nicolas.meric · 2021-12-13T16:23:45Z

nicolas.meric commented

2021-12-13 16:23:45 +00:00

No description provided.

nicolas.meric added 2 commits 2021-12-13 16:23:47 +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

541d2711bd Clean Up ISA check functions

Also remove some dead code

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

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

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

adbrucker added 1 commit 2021-12-15 22:25:24 +00:00

a2673b0825 Merge branch 'master' into clean-up-isa-check-functions

adbrucker referenced this issue from a commit

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

Merge pull request 'clean-up-isa-check-functions' (#7) from nicolas.meric/Isabelle_DOF:clean-up-isa-check-functions into master

adbrucker merged commit 9632c0810b into master

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

Sign in to join this conversation.

No reviewers

No Label

No Milestone

No Assignees

2 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#7