Custom query (544 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 544)

1 2 3 4 5 6

Status: closed (54 matches)

Ticket Summary Owner Type Priority Component Version
#17126 Command and command line option for global timeout multiplier. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17137 More tactical about goal selections Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17139 Multiple require at once. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17151 Abstract theories Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17158 "<-" for predicates when cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17159 expect should support goal selection Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17165 not-to-be-proved lemmas Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17166 missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17167 Better localization of errors when typing a proof-term Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17170 Introduce theory for product distribution Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17171 mode similar to nocheck that tries smt calls and just prints the locations for the failing calls Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17173 alternative to "require A; clone export A as B" that does not add A to SMT context enhancement 3 EasyCrypt pre-1.x
#17176 [print] should display types even on fixpoints Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17179 `done` should close goals with a direct contradiction in its env. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17185 Anomalies should give rise to a "This is a bug, please report."-type message. Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17189 Syntax for referring to *local* variables by their long name Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17196 Vernacular command for dumping env. as a Why3 task. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17201 `x-y` and `x + -y` should be convertible Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17204 Syntax for ignoring the return value of a procedure call Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#17220 Shorthand "by" syntax should be supported for "realize" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17221 parsing change allowing lemma ... by tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17227 Procedures with unit return type should be allowed to return `tt' Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17230 unhelpful error message when there are two matching operators with needed type Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17231 check for datatype being inhabited isn't complete, but error message suggests it is Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17232 weirdness involving redefining (=) or defining (<>) enhancement 3 EasyCrypt pre-1.x
#17234 Allow omission of a procedure's return type when it can be inferred Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17242 `print` should display `nosmt` info Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17247 Interactive proof realisation for `instance` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17248 More precise error messages when non-interactive realization fails Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17249 `AlgTactic` && `Ring` should agree on their axioms. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17258 Intro pattern for hypothesis duplication Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17266 Clear goal window when no more goals Pierre-Yves Strub enhancement 2 ProofGeneral pre-1.x
#17280 Parse-only abbreviations Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17284 Support for `={<expr>}` in equiv contracts Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17299 Transitivity using an equiv enhancement 3 EasyCrypt phl
#17314 Syntax variants of multiple argument module types don't match ones for parameterized modules Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17321 `case @[ambient]` needs its syntax unified with that of ambient `case` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17327 Variants of `<*>` with preference Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17328 `_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed enhancement 3 EasyCrypt pre-1.x
#17331 Tactic arguments for the `exists` tactic should not be comma-separated Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17332 Better localisation when a pattern cannot be infered Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17333 We need a `pragma` to stop EasyCrypt from reducing `b => false` into `!b`. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17336 `inline` procedure selection by code position Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17338 misspelled pragmas are not reported Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17359 `rewrite ?lem` should fail (hard) if `lem` does not exist in scope enhancement 3 EasyCrypt pre-1.x
#17362 wildcard syntax for SMT provers in prover [...] enhancement 3 EasyCrypt pre-1.x
#17371 new option for smt Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17372 "" and "!" semantic for smt Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17375 `include` command for modules / module types Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17377 characterization lemmas for <=> and \proper Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17397 odd scoping when overwriting operator in theory cloning enhancement 3 EasyCrypt pre-1.x
#17352 Question about run easycrypt task 3 EasyCrypt pre-1.x

Status: new (46 matches)

Ticket Summary Owner Type Priority Component Version
#17077 No more direct access to stdlib paths Pierre-Yves Strub defect 4 Internals pre-1.x
#17192 Problem with `glob` and type inference defect 3 EasyCrypt pre-1.x
#17215 Issues with module typing when functor parameters are themselves functors defect 3 EasyCrypt pre-1.x
#17246 `rewrite`, apply, ... in contracts defect 3 EasyCrypt pre-1.x
#17257 `/=` is too weak. defect 3 EasyCrypt pre-1.x
#17283 pattern matching complexity problem defect 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
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 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
#17346 have access to notation in ml defect 3 EasyCrypt pre-1.x
#17348 Intro-pattern `|>` might transform a provable goal to a non-provable one defect 3 EasyCrypt pre-1.x
#17366 crush losing some context on intermediate substitutions defect 3 EasyCrypt pre-1.x
#17386 crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal defect 3 EasyCrypt pre-1.x
#17390 problem with use of match on expression involving polymorphic operator/abbreviation defect 3 EasyCrypt pre-1.x
#17395 when cloning operators, lemmas may need to be turned into axioms defect 3 EasyCrypt pre-1.x
#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
#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
#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
#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
#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
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.