Replace Myth with Gallina Synthesizer
Closed this issue · 1 comments
AishwaryaSivaraman commented
We currently use myth to synthesize terms, but myth only supports a subset of the ocaml. This leads to a number of translation issues. We need to replace this with the new gallina synthesizer (being developed in https://github.com/qsctr/coq-synth).
We need to integrate coq-synth to lfind as an external binary call. If we try to call coq-synth as a library we face dependency issues with lfind plugin environment.
Similar to how we provide definitions and examples to lfind, we need to provide examples to coq-synth (see qsctr/coq-synth#1).