Basile Clément comments

Repositories
Issues
Comments

Results 182 comments of


                                            Basile Clément

Loading preludes after statements that must be processed in start mode

Ah, that's a good point. I guess that more specifically we should process preludes immediately after the `start` -> `assert` transition — I don't remember if we have a mechanism...

Incompleteness example for record theory (with quantifiers)

What about initializing the variables in CC(X) even if they only appear below quantifiers (we probably don't want to initialize variables that are truly unused)? It's a bit weird that...