basic): make decreasing induction eliminate to Sort
#1032

Merged

feat(data/nat/basic): make decreasing induction eliminate to Sort #1032

mergify merged 4 commits into master from decreasing_induction

add interface for decreasing_induction to Sort

287e331c

fpvandoorn requested a review 6 years ago

make decreasing_induction a def

0d064482

ChrisHughes24 commented on 2019-05-15

add simp tags and explicit type

489361fc

ChrisHughes24 approved these changes on 2019-05-16

ChrisHughes24 added ready-to-merge

Merge branch 'master' into 'decreasing_induction'

195cf43c

mergify merged def48b06 into master 6 years ago

mergify deleted the decreasing_induction branch 6 years ago

Reviewers

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone