trlc
trlc copied to clipboard
Treat Requirements Like Code
We can model decimals as integers and then divide them by a suitably large power of ten. This is not sound, but it is then complete, which may be in...
There are two copies of Nested_Lexer, working differently. This is not great.
We can check if a reference is `null` or not `null`. But we cannot check if a certain reference is there or not, because in the check file the symbol...
We could support something like this: ``` checks T { let { fraction = a / b } 1
This add CVC5 API support on Windows, making the external binary unnecessary. Because CVC5 packaging changed we now need a special script to fetch it. We can now also support...
In some scenarios, calling TRLC and piping the output to head creates a crash: ``` $ trlc | head T foo1 {x = 1} ^^^^ ./foo.trlc:2: check warning: potato T...
#12
It would be nice to be able to do this: ```trlc T Example { section_reference = 5.5.3 } ``` For a detailed proposal see https://github.com/florianschanda/trlc/blob/main/language-reference-manual/proposal-dot-separators.md
Having written several complex checks, its clear to me that the existing format is too simple, quickly resulting in repeated constructs. I suggest a new form: ``` type T {...