Agda icon indicating copy to clipboard operation
Agda copied to clipboard
verified publisher icon HoTT-Intro

Build with Agda 2.6.3

Open andreasabel opened this issue 1 month ago • 1 comments

  • Remove trailing whitespace (Just for one module which I touched.)

The following commits make all.agda build with Agda 2.6.3 (if I comment out OEIS-A000001.agda which exceeded my patience).

  • Add --guardedness flag needed for Agda 2.6.3 and up

  • INLINE composition to satify termination checker of Agda 2.6.3 and up

  • Disable extra.flat-modality not working with Agda 2.6.3 and up Agda rejects some definitions here, it is not clear to me whether Agda is right or whether this is a regression in Agda 2.6.3.

There is a regression in Agda 2.6.4 that causes an internal error. I have not investigated how to work around this one.

andreasabel avatar Dec 03 '25 16:12 andreasabel

@EgbertRijke : the regression of 2.6.4 will be fixed in Agda 2.9.0

  • agda/agda#8263
  • https://github.com/agda/agda/pull/8267

andreasabel avatar Dec 06 '25 14:12 andreasabel