Add missing Bind Scope for fin

This allows for automatic declaration of fin_scope when in a function argument of type fin n. For example in a defined function f {n}: fin n → T, you can now do f 45 instead of f 45%fin (assuming the n can be deduced of course). This might be a breaking change in very weird circumstances, but it otherwise allows a more convenient use of the fin notations.

added 1 commit

• bbe2655a - Add missing Bind Scope for fin

Compare with previous version

I agree with this change.

It needs a CHANGELOG entry, and perhaps a test?

added 22 commits

• bbe2655a...b9418660 - 21 commits from branch iris:master
• 4e4bd72b - Add missing Bind Scope for fin

Compare with previous version

I rebased, added a CHANGELOG entry and a test

resolved all threads

added 1 commit

• d470c5a6 - Comment.

Compare with previous version

added 18 commits

• d470c5a6...db81d6be - 17 commits from branch iris:master
• 1ee892d6 - Add missing Bind Scope for fin

Compare with previous version

resolved all threads

resolved all threads

added 1 commit

• 865f16d0 - More consistent CHANGELOG.

Compare with previous version

enabled an automatic merge when the pipeline for 865f16d0 succeeds

Thanks a lot. Going to merge.

mentioned in commit a2d0702e

merged