SeLFiE: LiFtEr: detect constants defined by inductive_set

data61 / PSL

Other

65 stars 9 forks source link

SeLFiE: LiFtEr: detect constants defined by inductive_set #127

Open yutakang opened 4 years ago

yutakang commented 4 years ago

By checking the corresponding .intros theorems that have Set.member as the outermost constant or as the outermost constant within the conclusion of a meta-implication.

yutakang commented 4 years ago

Done for now in 4e50b0c8add2e1138bc4ccfd3717a073357671fa.

But we can make it more stable using SeLFiE.