Skip to content

Implement meson_split_limit for meson #2062

Description

@ordinarymath

REPEAT(FIRST_X_ASSUM
((DISJ_CASES_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC)) THEN

This needs to be done like

Meson.SPLIT_TAC (!meson_split_limit) THEN
  let rec SPLIT_TAC n g =
    ((FIRST_X_ASSUM(CONJUNCTS_THEN' ASSUME_TAC) THEN SPLIT_TAC n) ORELSE
     (if n > 0 then FIRST_X_ASSUM DISJ_CASES_TAC THEN SPLIT_TAC (n - 1)
      else NO_TAC) ORELSE
     ALL_TAC) g

see https://github.com/jrh13/hol-light/blob/2a1cea8f1cb7f3885a60d947ba06eabac6ec1d32/meson.ml

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions