Skip to content

[ refactor ] make i ≢ j argument to Data.Fin.Base.punchOut irrelevant#2790

Closed
jamesmckinna wants to merge 19 commits into
agda:masterfrom
jamesmckinna:Fin-punchOut-properties
Closed

[ refactor ] make i ≢ j argument to Data.Fin.Base.punchOut irrelevant#2790
jamesmckinna wants to merge 19 commits into
agda:masterfrom
jamesmckinna:Fin-punchOut-properties