agda-stdlib [ new ] notions of finiteness

A subset of #2017 containing minimal changes related to finiteness

Jul 13 '23 20:07 Saransh-cpp

This PR on its own fails the “definitions should come with proofs” test, but maybe it's permissible with the promise of proofs in a later PR. We'll have to let the maintainers decide.

Jul 13 '23 22:07 laMudri

Yes, that is very true. I just don't how to include the proofs without bringing in a lot more changes (which should be in separate PRs according to the discussions in #2017).

Jul 13 '23 22:07 Saransh-cpp

(Overlooked in yesterday's meeting) Suggest at the very least that we bump this to v2.2, or even close (cf. #2005 ) until/unless someone comes along able to pick up the slack?

Jun 06 '24 07:06 jamesmckinna

I put it in v2.2 as I really would like to push this through.

Jun 07 '24 02:06 JacquesCarette

I put it in v2.2 as I really would like to push this through.

Comments on notation. I'd like to see this too, but as a fresh addition, we should try to get a 'convenient'/usable/memorable syntax/naming convention fixed before committing...

Aug 31 '24 09:08 jamesmckinna

I've converted this to a draft. @JacquesCarette when it's ready to review properly, turn it back again :+1:

Sep 03 '24 01:09 MatthewDaggitt

We've decided to close this for now, in favour of the "project issue #2511 " as it's a bigger deal.

Dec 06 '24 16:12 JacquesCarette