Logipedia icon indicating copy to clipboard operation
Logipedia copied to clipboard

Published 20 hours ago • verified publisher icon Deducteam

def_beta_conv.ml

Open francoisthire opened this issue 5 years ago • 1 comments

Why this file has been comitted?

francoisthire avatar Jan 29 '20 07:01 francoisthire

As far as I understand, this is needed by the hol light export (Emilie knows that better): it must be downloaded with hol light files. There should be a note somewhere in the documentation to explain that. And it should be moved to utils or something of the kind.

gabrielhdt avatar Jan 29 '20 09:01 gabrielhdt