search

openai / lean-gym

Apache License 2.0
150 stars 31 forks source link

[util/tactic] use `expr.reduce_let` in `tactic_hash` #2

Closed jesse-michael-han closed 3 years ago

jesse-michael-han commented 3 years ago

also fix a bug with goal hashing

jesse-michael-han commented 3 years ago

cc @spolu