#17185 |
Anomalies should give rise to a "This is a bug, please report."-type message.
|
Pierre-Yves Strub
|
enhancement
|
1
|
pre-1.x
|
trivial
|
#17189 |
Syntax for referring to *local* variables by their long name
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17196 |
Vernacular command for dumping env. as a Why3 task.
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17201 |
`x-y` and `x + -y` should be convertible
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17204 |
Syntax for ignoring the return value of a procedure call
|
Pierre-Yves Strub
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17220 |
Shorthand "by" syntax should be supported for "realize"
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17221 |
parsing change allowing lemma ... by tactics
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17227 |
Procedures with unit return type should be allowed to return `tt'
|
Pierre-Yves Strub
|
enhancement
|
2
|
pre-1.x
|
minor
|
#17230 |
unhelpful error message when there are two matching operators with needed type
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17231 |
check for datatype being inhabited isn't complete, but error message suggests it is
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17232 |
weirdness involving redefining (=) or defining (<>)
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17234 |
Allow omission of a procedure's return type when it can be inferred
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17242 |
`print` should display `nosmt` info
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17247 |
Interactive proof realisation for `instance`
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17248 |
More precise error messages when non-interactive realization fails
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17249 |
`AlgTactic` && `Ring` should agree on their axioms.
|
Pierre-Yves Strub
|
enhancement
|
2
|
pre-1.x
|
normal
|
#17258 |
Intro pattern for hypothesis duplication
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17280 |
Parse-only abbreviations
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17284 |
Support for `={<expr>}` in equiv contracts
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17299 |
Transitivity using an equiv
|
|
enhancement
|
3
|
phl
|
normal
|
#17314 |
Syntax variants of multiple argument module types don't match ones for parameterized modules
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17321 |
`case @[ambient]` needs its syntax unified with that of ambient `case`
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
trivial
|
#17327 |
Variants of `<*>` with preference
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17328 |
`_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17331 |
Tactic arguments for the `exists` tactic should not be comma-separated
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17332 |
Better localisation when a pattern cannot be infered
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17333 |
We need a `pragma` to stop EasyCrypt from reducing `b => false` into `!b`.
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17336 |
`inline` procedure selection by code position
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17338 |
misspelled pragmas are not reported
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17359 |
`rewrite ?lem` should fail (hard) if `lem` does not exist in scope
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17362 |
wildcard syntax for SMT provers in prover [...]
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17371 |
new option for smt
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17372 |
"" and "!" semantic for smt
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17375 |
`include` command for modules / module types
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17376 |
behaviour of module type include in functor types
|
Benjamin Grégoire
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17377 |
characterization lemmas for <=> and \proper
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17397 |
odd scoping when overwriting operator in theory cloning
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17403 |
Support for `move/(_ _ x): H=> H`
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17352 |
Question about run easycrypt
|
|
task
|
3
|
pre-1.x
|
normal
|
#17192 |
Problem with `glob` and type inference
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17215 |
Issues with module typing when functor parameters are themselves functors
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17246 |
`rewrite`, apply, ... in contracts
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17257 |
`/=` is too weak.
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17283 |
pattern matching complexity problem
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17287 |
Program transformation tactics should not `anomaly` without a side in pRHL
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17288 |
EasyCrypt crashes when printing required abstract theory IterProc
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17316 |
[smt (@Theory)] should force the use of axioms marked as `nosmt`
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17322 |
use of side with HL version of while tactic should be syntax error
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17346 |
have access to notation in ml
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17348 |
Intro-pattern `|>` might transform a provable goal to a non-provable one
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17366 |
crush losing some context on intermediate substitutions
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17386 |
crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17390 |
problem with use of match on expression involving polymorphic operator/abbreviation
|
|
defect
|
3
|
pre-1.x
|
normal
|
#17395 |
when cloning operators, lemmas may need to be turned into axioms
|
|
defect
|
3
|
pre-1.x
|
normal
|
#16103 |
scoping issue with theories
|
|
enhancement
|
3
|
pre-1.x
|
|
#16648 |
Make notations and tactics on distributions and functions a bit more uniform.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#16912 |
Lifting the "collection update" statements to tuples
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#16987 |
Move facts from precondition to context
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17022 |
Pattern-matching on variables in judgments and probability expressions
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17036 |
Instantiating abstract modules: warnings and interactive justification
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17037 |
Poor error message for module restriction example
|
Pierre-Yves Strub
|
enhancement
|
2
|
pre-1.x
|
minor
|
#17045 |
Rewriting procedures in probability expressions directly from an equivalence
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17082 |
SMT tactic should be interruptable.
|
Pierre-Yves Strub
|
enhancement
|
4
|
pre-1.x
|
normal
|
#17085 |
Generic Notations
|
Pierre-Yves Strub
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17086 |
Generalize [rewrite Pr]
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17088 |
`case !a` should reduce to proving `a`
|
Pierre-Yves Strub
|
enhancement
|
2
|
pre-1.x
|
normal
|
#17090 |
Selecting procedure(s) to [inline] by position
|
|
enhancement
|
2
|
pre-1.x
|
normal
|
#17105 |
[transitivity] for phoare and hoare
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17113 |
Decide what to do on rewrite with defined head symbols
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17136 |
variant of seq to deal with large preconditions
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17140 |
Pattern matching should make use of simplification rules.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17149 |
Expand glob A for concrete module
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17156 |
New vernacular command: `print axiom`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17164 |
behavior of -check-all
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17169 |
Anonymous functor arguments: passing procedures to functors directly
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17175 |
Direct intro on negative goals
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17183 |
Variant of `sim` that works modulo inlining.
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17197 |
Asserts in equivalence proofs
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17202 |
Add seq* tactic
|
|
enhancement
|
3
|
pre-1.x
|
major
|
#17210 |
Pattern-matching for pairs in operator arguments
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17217 |
need better error message when attempting to apply lemma to goal that isn't a judgment
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17218 |
proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17225 |
Explore reproducible smt calls
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17239 |
Mutual inductive types.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17245 |
Formula manipulation commands (for `conseq` and `seq`)
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17251 |
print Self
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17267 |
`auto` with `call`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17279 |
Improve `invalid goal shape` error messages for variants of `byequiv`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17281 |
Several problems with `apply` in program logics
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17285 |
Transitivity on procedures should support inferring contracts from `equiv` lemmas.
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17286 |
pRHL `apply` should have a framing variant
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17290 |
`n!->>` should work
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17295 |
local ops
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17297 |
Allow the optional use of undeclared variables in procedures
|
|
enhancement
|
1
|
pre-1.x
|
normal
|
#17298 |
Super rnd
|
|
enhancement
|
4
|
phl
|
blocker
|
#17301 |
Applicative view for `if then else`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17305 |
proc* in eager case needlessly assigns result of procedures returning unit to variables
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17307 |
Coq style Locate
|
|
enhancement
|
1
|
pre-1.x
|
minor
|
#17311 |
`smt (@Self)`
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
#17317 |
`search` should work somewhat better with abbreviations
|
|
enhancement
|
3
|
pre-1.x
|
normal
|
(more results for this group on next page)
|