Alessandro Coglio

Loading a file with the content below in an ACL2 session and then opening test-manual/index.html (tried Safari and Firefox) does not show the definitions of F and G in their...

Fixtype of lists of strings fails

7

[This page](http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/?topic=FTY____DEFLIST) shows, at the very end, a form to create a fixing function for the existing STRING-LISTP predicate. However, the following fails (starting in a fresh ACL2 session): (include-book...

[Feature] Use a keyword to designate external functions?

1

There are currently two kinds of functions in Leo: - External functions, callable "from outside" (e.g. via input files), and designated via the `@program` annotation. - Internal functions, also called...

According to [this text in the Rust Book](https://doc.rust-lang.org/book/ch07-05-separating-modules-into-different-files.html#alternate-file-paths), the currently preferred path for the code in a module `mymodule` is `.../mymodule.rs` rather than `.../mymodule/mod.rs`. As noted in the referenced text,...

Consider this example: ``` > cat src/main.leo @program function main(a: u32) -> u32 { return a + 1u32; // not what it looks like } > cat inputs/backspace.in [main] a:...

## 🚀 Feature There seems to be at least two decisions: - JSON format or our own format/grammar. - Association of public/private/constant designations to inputs. The second decision consists in...

[Feature] Should line terminators in string literals be allowed or disallowed?

2

## 🚀 Feature This is related to #1717. Here 'line terminator' does not refer to the escapes `\n` and `\r`, which should arguably be allowed, but actual line breaks in...

[Feature] Treatment of statically dead code

2

## 🚀 Feature In a block like ``` { let x: u8 = 3u8; return x; x = 3u32; } ``` the assignment (i.e. the 3rd statement) is statically dead...

[Bug] Discrepancy between grammar and parser for input items

1

## 🐛 Bug Report The ABNF input grammar file defines ``` input-item = identifier ":" input-type "=" input-expression ";" ``` while the parser accepts an option `const`/`constant`/`public` before the identifier:...

## 🚀 Feature This is in `positive_numbers.rs` in the `ast` module. While 0 is regarded as 'positive' in certain contexts, more generally 'positive' means 'greater than 0'. So `Positive` in...