mathlib3
feat(tactic/squeeze): remove noise from output
#1047
Merged

feat(tactic/squeeze): remove noise from output #1047

cipher1024 merged 1 commit into master from squeeze-noise
cipher1024
cipher1024 feat(tactic/squeeze): remove noise from output
e2caa45a
cipher1024 cipher1024 requested a review 6 years ago
cipher1024 cipher1024 requested a review from kim-em kim-em 6 years ago
cipher1024 cipher1024 requested a review from digama0 digama0 6 years ago
cipher1024 cipher1024 merged 73c3f717 into master 6 years ago
cipher1024 cipher1024 deleted the squeeze-noise branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone