[acl2/acl2] 16761b: [FTY] Add maps from strings to strings.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 16761be75689941a1f54f9a1d4c12ccf0c6bd4af
https://github.com/acl2/acl2/commit/16761be75689941a1f54f9a1d4c12ccf0c6bd4af
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
A books/kestrel/fty/string-string-map.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add maps from strings to strings.


Commit: b7eb6ae88d88c50f40873cd9a2417b457fe39217
https://github.com/acl2/acl2/commit/b7eb6ae88d88c50f40873cd9a2417b457fe39217
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
A books/kestrel/fty/string-string-map.lisp
M books/kestrel/fty/top.lisp

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


Commit: bd14f43150b4eba3e2c56dbda6c1e276e4731bf7
https://github.com/acl2/acl2/commit/bd14f43150b4eba3e2c56dbda6c1e276e4731bf7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import symbol into package.


Commit: 9d901e79acf63dbbd3f3403469940fbed61d3a6e
https://github.com/acl2/acl2/commit/9d901e79acf63dbbd3f3403469940fbed61d3a6e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-substitution-operations.lisp

Log Message:
-----------
[Remora] Add some variable renaming operations.


Commit: 09571e15d68fe8b79628f529bdadc805647ac439
https://github.com/acl2/acl2/commit/09571e15d68fe8b79628f529bdadc805647ac439
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
M books/kestrel/fty/string-string-map.lisp

Log Message:
-----------
[FTY] Add a theorem.


Commit: e52baeec993cbc56993b2e1a588e79c1a247ddd6
https://github.com/acl2/acl2/commit/e52baeec993cbc56993b2e1a588e79c1a247ddd6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp

Log Message:
-----------
[Remora] Add theorem.


Commit: c3a3ff0d019c892c686a7a3f645b6af746c596dc
https://github.com/acl2/acl2/commit/c3a3ff0d019c892c686a7a3f645b6af746c596dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add type checking of unboxing expressions.


Commit: 30ff297b8b7fd0c4cde024044a205b83739f2005
https://github.com/acl2/acl2/commit/30ff297b8b7fd0c4cde024044a205b83739f2005
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add type checking of term abstractions.


Commit: ee3ec8285ed039fc3fb6cfec652a5e903f596b4f
https://github.com/acl2/acl2/commit/ee3ec8285ed039fc3fb6cfec652a5e903f596b4f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add type checking of type abstractions.


Commit: 12eee3efa7abc2ec60d9715146e507148891012d
https://github.com/acl2/acl2/commit/12eee3efa7abc2ec60d9715146e507148891012d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add type checking of index abstractions.


Commit: 29d84b71f6c2ebaabe019ffebec1838a2c8c739c
https://github.com/acl2/acl2/commit/29d84b71f6c2ebaabe019ffebec1838a2c8c739c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add type checking of box construct.

Also rework some theorems.


Commit: c92d5c313989131ef7a20cc76cf4daea4a3122b7
https://github.com/acl2/acl2/commit/c92d5c313989131ef7a20cc76cf4daea4a3122b7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf

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


Commit: 80d1b9cc60ad92489c7e110a86f385d8f23cc657
https://github.com/acl2/acl2/commit/80d1b9cc60ad92489c7e110a86f385d8f23cc657
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add a theorem about equivalent types.


Commit: 3dfa32100840f6de85c5ca8991828467282da312
https://github.com/acl2/acl2/commit/3dfa32100840f6de85c5ca8991828467282da312
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Use type equivalence for term application.


Commit: c60de5dfe39f72a0f3cfe87bf52d37dc2253e5f3
https://github.com/acl2/acl2/commit/c60de5dfe39f72a0f3cfe87bf52d37dc2253e5f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:

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


Compare: https://github.com/acl2/acl2/compare/78adc18e6779...c60de5dfe39f

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

[Alessandro Coglio]

Branch: refs/heads/testing