search

data61 / PSL

Other
65 stars 9 forks source link

semantic_induct, SeLFiE: smart construction should handle inductive_set differently. #180

Closed yutakang closed 3 years ago

yutakang commented 3 years ago

The SeLFiE interpreter should also treat the rule name differently: the induct tactic does not take .induct.

For now, the smart construction does not have to produce induction terms for set-rules.

yutakang commented 3 years ago

agh... the "fix" in 577935ff092d62faceb83f9a17c980dbbcd2fca4 is not good enough.

We have to change datatype induct_arguments = Induct_Arguments of {ons: strings, arbs: strings, rules: strings}; in SeLFiE_Util in SeLFiE/Util.ML and the relevant functions in the same structure such as induct_arguments_to_string, so that induct_arguments_to_string can produce induct ... set: ... for constants defined by the inductive_set keyword.

yutakang commented 3 years ago

Done.