search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
41 stars 24 forks source link

Avoid admits in symmetry test code #33

Closed tchajed closed 4 years ago

tchajed commented 4 years ago

This is just so that our artifacts don't have any admits that would worry reviewers.

tchajed commented 4 years ago

Oops I already did this in #30. It seemed familiar but I didn't remember finishing it up...