Some work on formalizing Suffix (re: #517)#551

Merged

MatthewDaggitt merged 12 commits intoagda:masterfrom

iitalics:suffix

Jan 12, 2019

Commits on Dec 29, 2018

[ re #517 ] Definition of heterogeneous Suffix and SuffixView

Milo Turner
authored and
iitalics
committed
Add suffix tail, map

Milo Turner
authored and
iitalics
committed
Added some Suffix properties

Milo Turner
authored and
iitalics
committed
Implement Suffix toPointwise and some theorems that depends on it

Milo Turner
authored and
iitalics
committed
Add theorems for converting between Suffix/Prefix by reversing

Milo Turner
authored and
iitalics
committed
Implement Suffix antisym

Milo Turner
authored and
iitalics
committed
Clean up a bit by using 'Pointwise-length' and 'sym'

Milo Turner
authored and
iitalics
committed
Positive/negative variations of fromPrefix/toPrefix

Milo Turner
authored and
iitalics
committed
Add Suffix irrelevance and decidability

Milo Turner
authored and
iitalics
committed
Minor clean up using Function._$_

Milo Turner
authored and
iitalics
committed
Add new proofs to Data.List.Relation.Pointwise
iitalics
committed
Use newly moved Pointwise properties in Suffix properties
iitalics
committed