Custom query (122 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 122)

1 2

Status: accepted (11 matches)

Ticket Summary Owner Type Priority Component Version
#16113 <top> in printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17024 Pattern matching should try to infer memory and module parameters Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17034 Generalizing loop fusion Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17040 Syntactic sugar for nested if-then-else statements. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17042 Pattern matching in non-normal form. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17070 better error message when difference between goal and lemma is tiny Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17141 Wrong module type annotations accepted Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17195 Swap with 2 args move as far down as possible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17250 off-by-one error in swap Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17309 `rewrite /F` when F is a fixpoint should simplify selected occurence for head-iota reduction. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17378 Proof of false using smt and Eprover. Pierre-Yves Strub defect 5 EasyCrypt pre-1.x

Status: assigned (28 matches)

Ticket Summary Owner Type Priority Component Version
#17117 Warning when restrictions over an adversary are empty Benjamin Grégoire enhancement 2 EasyCrypt pre-1.x
#17181 slow rewriting for large expressions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17207 Applicative view Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17222 local clones do not disappear from the environment on section end Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17240 Syntactic sugar for proc. that reduces to a call to an external proc. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17253 EasyCrypt should fail gracefully when applying a tactic on a solved goal. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17255 Missing unification in `clone...with...` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17256 apply/rewrite should work modulo zeta-reduction. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17261 `rewrite -/(f _)` should not match its own unfoldings. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17262 Add the possibility to add rewrite hints to rewrite hint databases. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17263 Multiple incompleteness in `apply` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17264 Add the possibility to clear lemmas when closing a theory. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17265 `goal` vernacular command Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17268 Add a tactical that fails when no progress is done. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17269 Add notations for >/>= Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17270 `done` should close a goal when `false` is a local hyp. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17308 `rewrite !(A,B)` loops when `B` is not known about Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17310 Top-level command to print various databases (exact, rewrite, ...) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17319 Anomaly triggered by `smt` defect 3 EasyCrypt pre-1.x
#17334 this message need more information: cannot infer all placeholders Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17335 the formula contains free type variables Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17343 (Optional) warning for old syntax Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17345 Bad printing Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#17347 Search with notations is broken. Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17364 Internals: use Batteries maps instead of Why3 ones. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17160 Call SMT in parallels. Pierre-Yves Strub enhancement 2 Internals pre-1.x

Status: new (61 matches)

Ticket Summary Owner Type Priority Component Version
#16103 scoping issue with theories enhancement 3 EasyCrypt pre-1.x
#16648 Make notations and tactics on distributions and functions a bit more uniform. enhancement 3 EasyCrypt pre-1.x
#16912 Lifting the "collection update" statements to tuples enhancement 1 EasyCrypt pre-1.x
#16987 Move facts from precondition to context enhancement 3 EasyCrypt pre-1.x
#17002 Better section && cloning support Pierre-Yves Strub task 3 EasyCrypt pre-1.x
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 EasyCrypt pre-1.x
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 EasyCrypt pre-1.x
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 EasyCrypt pre-1.x
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17085 Generic Notations Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17086 Generalize [rewrite Pr] enhancement 3 EasyCrypt pre-1.x
#17088 `case !a` should reduce to proving `a` Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17090 Selecting procedure(s) to [inline] by position enhancement 2 EasyCrypt pre-1.x
#17105 [transitivity] for phoare and hoare enhancement 3 EasyCrypt pre-1.x
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 EasyCrypt pre-1.x
#17136 variant of seq to deal with large preconditions enhancement 3 EasyCrypt pre-1.x
#17140 Pattern matching should make use of simplification rules. enhancement 3 EasyCrypt pre-1.x
#17149 Expand glob A for concrete module enhancement 3 EasyCrypt pre-1.x
#17156 New vernacular command: `print axiom` enhancement 3 EasyCrypt pre-1.x
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. task 4 EasyCrypt pre-1.x
#17164 behavior of -check-all enhancement 3 EasyCrypt pre-1.x
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 EasyCrypt pre-1.x
#17175 Direct intro on negative goals enhancement 3 EasyCrypt pre-1.x
#17183 Variant of `sim` that works modulo inlining. enhancement 1 EasyCrypt pre-1.x
#17192 Problem with `glob` and type inference defect 3 EasyCrypt pre-1.x
#17197 Asserts in equivalence proofs enhancement 3 EasyCrypt pre-1.x
#17202 Add seq* tactic enhancement 3 EasyCrypt pre-1.x
#17210 Pattern-matching for pairs in operator arguments enhancement 3 EasyCrypt pre-1.x
#17215 Issues with module typing when functor parameters are themselves functors defect 3 EasyCrypt pre-1.x
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 EasyCrypt pre-1.x
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 EasyCrypt pre-1.x
#17225 Explore reproducible smt calls enhancement 3 EasyCrypt pre-1.x
#17239 Mutual inductive types. enhancement 3 EasyCrypt pre-1.x
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 EasyCrypt pre-1.x
#17246 `rewrite`, apply, ... in contracts defect 3 EasyCrypt pre-1.x
#17251 print Self enhancement 3 EasyCrypt pre-1.x
#17257 `/=` is too weak. defect 3 EasyCrypt pre-1.x
#17267 `auto` with `call` enhancement 3 EasyCrypt pre-1.x
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 EasyCrypt pre-1.x
#17281 Several problems with `apply` in program logics enhancement 3 EasyCrypt pre-1.x
#17282 call should not work task 3 EasyCrypt phl
#17283 pattern matching complexity problem defect 3 EasyCrypt pre-1.x
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 EasyCrypt pre-1.x
#17286 pRHL `apply` should have a framing variant enhancement 3 EasyCrypt pre-1.x
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 EasyCrypt pre-1.x
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 EasyCrypt pre-1.x
#17290 `n!->>` should work enhancement 3 EasyCrypt pre-1.x
#17295 local ops enhancement 3 EasyCrypt pre-1.x
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 EasyCrypt pre-1.x
#17298 Super rnd enhancement 4 EasyCrypt phl
#17301 Applicative view for `if then else` enhancement 3 EasyCrypt pre-1.x
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 EasyCrypt pre-1.x
#17307 Coq style Locate enhancement 1 EasyCrypt pre-1.x
#17311 `smt (@Self)` enhancement 3 EasyCrypt pre-1.x
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 EasyCrypt pre-1.x
#17317 `search` should work somewhat better with abbreviations enhancement 3 EasyCrypt pre-1.x
#17322 use of side with HL version of while tactic should be syntax error defect 3 EasyCrypt pre-1.x
#17325 syntax marking end of cloning realization enhancement 3 EasyCrypt pre-1.x
#17337 substitutions should complain when substituting a locally defined variable enhancement 3 EasyCrypt pre-1.x
#17340 cfold should support variables (and more general terms). enhancement 3 EasyCrypt pre-1.x
(more results for this group on next page)
1 2
Note: See TracQuery for help on using queries.