[acl2/acl2] bcd767: [Remora] Fix bug in type checker.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: bcd7676d115da35c7737d61e9c1653df93d5da3f
https://github.com/acl2/acl2/commit/bcd7676d115da35c7737d61e9c1653df93d5da3f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Fix bug in type checker.

The types of the `let` bindings for functions need to be wrapped into scalar
arrays.

Thanks to Quan Luu for finding and reporting the issue.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Home: https://github.com/acl2/acl2
Commit: bcd7676d115da35c7737d61e9c1653df93d5da3f
https://github.com/acl2/acl2/commit/bcd7676d115da35c7737d61e9c1653df93d5da3f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Fix bug in type checker.

The types of the `let` bindings for functions need to be wrapped into scalar
arrays.

Thanks to Quan Luu for finding and reporting the issue.

Commit: 904acf589841f19d190da616dde7ffd2b96d7da2
https://github.com/acl2/acl2/commit/904acf589841f19d190da616dde7ffd2b96d7da2
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:

A books/projects/set-theory/reals/dedekind.lisp
A books/projects/set-theory/reals/negative.lisp
A books/projects/set-theory/reals/sum.lisp

Log Message:
-----------
Begin the development of reals in set theory via Dedekind cuts.

I've defined Dedekind cuts and their sum and negative, proving that
sum and negative preserve the property of being a Dedekind cut.
Proving this for the negative case was getting messy, so I got AI to
help as described in file
books/projects/set-theory/reals/negative.lisp.


Commit: e867f4eea54c35b062308fc1ca8992cc65cec58a
https://github.com/acl2/acl2/commit/e867f4eea54c35b062308fc1ca8992cc65cec58a
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:

A books/projects/set-theory/reals/cert.acl2

Log Message:
-----------
Added missing cert.acl2 file (not necessary when using cert.pl, though)


Commit: bcb63eea658f726faa308736f17f925da691a24b
https://github.com/acl2/acl2/commit/bcb63eea658f726faa308736f17f925da691a24b

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:

A books/projects/set-theory/reals/cert.acl2
A books/projects/set-theory/reals/dedekind.lisp
A books/projects/set-theory/reals/negative.lisp
A books/projects/set-theory/reals/sum.lisp

Log Message:
-----------
Merge.


Commit: 6be6c75484f70282ddc712cfe6346edec811b950
https://github.com/acl2/acl2/commit/6be6c75484f70282ddc712cfe6346edec811b950

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------

Merge.


Compare: https://github.com/acl2/acl2/compare/2a9a29745b6d...6be6c75484f7

[acl2buildserver]

Branch: refs/heads/master

Home: https://github.com/acl2/acl2
Commit: bcd7676d115da35c7737d61e9c1653df93d5da3f
https://github.com/acl2/acl2/commit/bcd7676d115da35c7737d61e9c1653df93d5da3f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Fix bug in type checker.

The types of the `let` bindings for functions need to be wrapped into scalar
arrays.

Thanks to Quan Luu for finding and reporting the issue.

Commit: 02922a01cb5fb2928c49f9dcbc2dc3c73d51f32e
https://github.com/acl2/acl2/commit/02922a01cb5fb2928c49f9dcbc2dc3c73d51f32e
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-07-01 (Wed, 01 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------

Merge commit 'bcd7676d115da35c7737d61e9c1653df93d5da3f' into HEAD


Compare: https://github.com/acl2/acl2/compare/e867f4eea54c...02922a01cb5f

[acl2buildserver]

Branch: refs/heads/testing