Define Sn as a HIT - Githubissues

vikraman / 2DTypes

Collaborative work on reversible computing

17 stars 1 forks source link

Define Sn as a HIT #32

Closed vikraman closed 3 years ago

vikraman commented 3 years ago

Fixes #8

inexxt commented 3 years ago

I wouldn't say I undestand the whole code, but - why is it not parametrised by n? (Such as the relation we've defined in here https://github.com/vikraman/2DTypes/commit/b6b6c35c255622294397bb188c14e579a1a88629 ?)

inexxt commented 3 years ago

I changed the definition to be parametrised by n (e.g. the generators being in Fin n instead of ℕ) - jus to show what I meant, not as a final statement. Please modify it as you like.

vikraman commented 3 years ago

Wouldn't it be better to just expand out the Fins like in LL ?