search

IBM / graph2tac

Graph-based neural tactic prediction models for Coq.
Apache License 2.0
8 stars 4 forks source link

more flexible tactic uniqueness filter #122

Closed mirefek closed 1 year ago

mirefek commented 1 year ago

exclude_unique_tactic: false ->required_tactic_occurrence: 1 exclude_unique_tactic: true ->required_tactic_occurrence: 2

tests pass

mirefek commented 1 year ago

There is no difference between 0 and 1.

mirefek commented 1 year ago

It was a bit easier to phrase the argument positively: "keep only tactics occuring at least k-times", and there is indeed no way to detect a tactic occuring 0 times.

jasonrute commented 1 year ago

Ok. I'll merge it.