Custom query (161 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (1 - 100 of 161)

1 2
Ticket Summary Status Owner Type Priority Milestone
#17378 Proof of false using smt and Eprover. accepted Pierre-Yves Strub defect 5 1.0
#17058 Improving the performance of the [smt] tactic new task 4 1.1
#17077 No more direct access to stdlib paths new Pierre-Yves Strub defect 4 1.0
#17082 SMT tactic should be interruptable. new Pierre-Yves Strub enhancement 4 1.0
#17131 Incompleteness of "call" assigned Benjamin Grégoire enhancement 4 1.1
#17141 Wrong module type annotations accepted accepted Pierre-Yves Strub defect 4 1.0
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. new task 4 1.0
#17298 Super rnd new enhancement 4 1.0
#16103 scoping issue with theories new enhancement 3 1.0
#16467 Allow rewriting bellow quantifiers new enhancement 3 1.1
#16485 Overconservative restriction check in the pHL and pRHL while loops assigned Benjamin Grégoire enhancement 3 1.1
#16648 Make notations and tactics on distributions and functions a bit more uniform. new enhancement 3 1.0
#16728 "call (_: bad, inv)" generates goals that are stronger than necessary assigned Benjamin Grégoire enhancement 3 1.1
#16750 match in procedure new enhancement 3 1.1
#16771 Generating recursors and induction principles with equality for datatypes new enhancement 3 1.1
#16835 Record updates new Pierre-Yves Strub enhancement 3 1.1
#16896 rcond on nested conditionals new enhancement 3 1.1
#16901 Generic oracle annotations new enhancement 3 1.1
#16934 Limit the introduction of fresh variables when inlining new enhancement 3 1.1
#16962 pred ... = ... axiomatized by ... new Pierre-Yves Strub enhancement 3 1.1
#16975 Improvements to the type system for expressions assigned Clément Sartori enhancement 3 1.1
#16987 Move facts from precondition to context new enhancement 3 1.0
#17000 Adding noops to align code in relational goals new enhancement 3 1.1
#17002 Better section && cloning support new Pierre-Yves Strub task 3 1.0
#17004 Improvements to FEL new task 3 1.1
#17019 Deprecating the hoare tactic - unifying with by<logic> and conseq new enhancement 3 1.1
#17020 Avoid internal use of simple defined notations new enhancement 3 1.1
#17022 Pattern-matching on variables in judgments and probability expressions new enhancement 3 1.0
#17024 Pattern matching should try to infer memory and module parameters accepted Pierre-Yves Strub enhancement 3 1.0
#17025 Pattern matching and sub-formulas extraction in hl/phl/prhl tactics. new Pierre-Yves Strub enhancement 3 1.1
#17034 Generalizing loop fusion accepted Pierre-Yves Strub enhancement 3 1.0
#17039 Contextual pattern matching accepted Charlie Root enhancement 3 1.1
#17040 Syntactic sugar for nested if-then-else statements. accepted Pierre-Yves Strub enhancement 3 1.0
#17041 Program logic {{{case}}} for inductives and inductive-likes reopened Pierre-Yves Strub enhancement 3 1.1
#17042 Pattern matching in non-normal form. accepted Pierre-Yves Strub enhancement 3 1.0
#17043 Aliasing module types (and functor types) new enhancement 3 1.1
#17062 Parser error when using inner module in apply new enhancement 3 1.1
#17063 Theory names aliasing new enhancement 3 1.1
#17070 better error message when difference between goal and lemma is tiny accepted Pierre-Yves Strub enhancement 3 1.0
#17076 [seq]-based [if] should work in Hoare and pHoare new Benjamin Grégoire enhancement 3 1.1
#17081 Operators/predicates on memories/modules. new task 3
#17085 Generic Notations new Pierre-Yves Strub enhancement 3 1.0
#17086 Generalize [rewrite Pr] new enhancement 3 1.0
#17103 Push glob normalization from pre-why3 call to the why3 module. new enhancement 3 1.1
#17105 [transitivity] for phoare and hoare new enhancement 3 1.0
#17111 Tactic for expression propagation new enhancement 3 1.1
#17113 Decide what to do on rewrite with defined head symbols new enhancement 3 1.0
#17136 variant of seq to deal with large preconditions new enhancement 3 1.0
#17140 Pattern matching should make use of simplification rules. new enhancement 3 1.0
#17149 Expand glob A for concrete module new enhancement 3 1.0
#17156 New vernacular command: `print axiom` new enhancement 3 1.0
#17164 behavior of -check-all new enhancement 3 1.0
#17169 Anonymous functor arguments: passing procedures to functors directly new enhancement 3 1.0
#17175 Direct intro on negative goals new enhancement 3 1.0
#17181 slow rewriting for large expressions assigned Pierre-Yves Strub defect 3 1.0
#17182 Renaming internal symbols on cloning reopened Pierre-Yves Strub enhancement 3 1.0
#17186 using [bypr] in odd way can result in badly formed goal reopened Pierre-Yves Strub defect 3 1.0
#17192 Problem with `glob` and type inference new defect 3 1.0
#17194 anomaly: EcHiGoal.LowApply.NoInstance (in byequiv) assigned Benjamin Grégoire defect 3 1.0
#17195 Swap with 2 args move as far down as possible accepted Pierre-Yves Strub enhancement 3 1.0
#17197 Asserts in equivalence proofs new enhancement 3 1.0
#17202 Add seq* tactic new enhancement 3 1.0
#17207 Applicative view assigned Pierre-Yves Strub enhancement 3 1.0
#17209 Remove the distinction between operators and predicates assigned Pierre-Yves Strub enhancement 3 1.1
#17210 Pattern-matching for pairs in operator arguments new enhancement 3 1.0
#17215 Issues with module typing when functor parameters are themselves functors new defect 3 1.0
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment new enhancement 3 1.0
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate new enhancement 3 1.0
#17222 local clones do not disappear from the environment on section end assigned Pierre-Yves Strub enhancement 3 1.0
#17225 Explore reproducible smt calls new enhancement 3 1.0
#17239 Mutual inductive types. new enhancement 3 1.0
#17240 Syntactic sugar for proc. that reduces to a call to an external proc. assigned Pierre-Yves Strub enhancement 3 1.0
#17245 Formula manipulation commands (for `conseq` and `seq`) new enhancement 3 1.0
#17246 `rewrite`, apply, ... in contracts new defect 3 1.0
#17250 off-by-one error in swap accepted Pierre-Yves Strub defect 3 1.0
#17251 print Self new enhancement 3 1.0
#17255 Missing unification in `clone...with...` assigned Pierre-Yves Strub enhancement 3 1.0
#17256 apply/rewrite should work modulo zeta-reduction. assigned Pierre-Yves Strub defect 3 1.0
#17257 `/=` is too weak. new defect 3 1.0
#17259 Theory of distribution (iso)morphisms new task 3 1.0
#17261 `rewrite -/(f _)` should not match its own unfoldings. assigned Pierre-Yves Strub defect 3 1.0
#17262 Add the possibility to add rewrite hints to rewrite hint databases. assigned Pierre-Yves Strub enhancement 3 1.0
#17263 Multiple incompleteness in `apply` assigned Pierre-Yves Strub defect 3 1.0
#17265 `goal` vernacular command assigned Pierre-Yves Strub defect 3 1.0
#17267 `auto` with `call` new enhancement 3 1.0
#17268 Add a tactical that fails when no progress is done. assigned Pierre-Yves Strub enhancement 3 1.0
#17269 Add notations for >/>= assigned Pierre-Yves Strub enhancement 3 1.0
#17270 `done` should close a goal when `false` is a local hyp. assigned Pierre-Yves Strub enhancement 3 1.0
#17271 Pattern matching should solve problems of the form `?f tj...tn ~ f t1 ... tn` assigned Pierre-Yves Strub enhancement 3 1.0
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` new enhancement 3 1.0
#17281 Several problems with `apply` in program logics new enhancement 3 1.0
#17282 call should not work new task 3 1.0
#17283 pattern matching complexity problem new defect 3 1.0
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. new enhancement 3 1.0
#17286 pRHL `apply` should have a framing variant new enhancement 3 1.0
#17287 Program transformation tactics should not `anomaly` without a side in pRHL new defect 3 1.0
#17288 EasyCrypt crashes when printing required abstract theory IterProc new defect 3 1.0
#17290 `n!->>` should work new enhancement 3 1.0
#17295 local ops new enhancement 3 1.0
#17301 Applicative view for `if then else` new enhancement 3 1.0
1 2
Note: See TracQuery for help on using queries.