Custom query (536 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (501 - 536 of 536)

1 2 3 4 5 6

Status: new (34 matches)

Ticket Summary Owner Type Priority Component Version
#17210 Pattern-matching for pairs in operator arguments enhancement 3 EasyCrypt pre-1.x
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 EasyCrypt pre-1.x
#17140 Pattern matching should make use of simplification rules. enhancement 3 EasyCrypt pre-1.x
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17374 pre-/post- should be implemented with an explicit memory enhancement 3 Internals pre-1.x
#17286 pRHL `apply` should have a framing variant enhancement 3 EasyCrypt pre-1.x
#17251 print Self enhancement 3 EasyCrypt pre-1.x
#17385 problem sending goal to SMT (involving inductive datatype and higher order function) defect 3 EasyCrypt pre-1.x
#17192 Problem with `glob` and type inference defect 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
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 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
#17246 `rewrite`, apply, ... in contracts defect 3 EasyCrypt pre-1.x
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 EasyCrypt pre-1.x
#17357 rnd tactic for aprhl enhancement 3 EasyCrypt pre-1.x
#16103 scoping issue with theories enhancement 3 EasyCrypt pre-1.x
#17317 `search` should work somewhat better with abbreviations enhancement 3 EasyCrypt pre-1.x
#17090 Selecting procedure(s) to [inline] by position enhancement 2 EasyCrypt pre-1.x
#17281 Several problems with `apply` in program logics enhancement 3 EasyCrypt pre-1.x
#17311 `smt (@Self)` enhancement 3 EasyCrypt pre-1.x
#17082 SMT tactic should be interruptable. Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 EasyCrypt pre-1.x
#17351 sp for aqeuiv goals enhancement 3 EasyCrypt pre-1.x
#17337 substitutions should complain when substituting a locally defined variable enhancement 3 EasyCrypt pre-1.x
#17298 Super rnd enhancement 4 EasyCrypt phl
#17325 syntax marking end of cloning realization enhancement 3 EasyCrypt pre-1.x
#17259 Theory of distribution (iso)morphisms task 3 Libraries pre-1.x
#17105 [transitivity] for phoare and hoare enhancement 3 EasyCrypt pre-1.x
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 EasyCrypt pre-1.x
#17344 Trees and polynomials enhancement 3 EasyCrypt pre-1.x
#17356 Two-sided `rcondx` enhancement 1 EasyCrypt pre-1.x
#17322 use of side with HL version of while tactic should be syntax error defect 3 EasyCrypt pre-1.x
#17136 variant of seq to deal with large preconditions enhancement 3 EasyCrypt pre-1.x
#17183 Variant of `sim` that works modulo inlining. enhancement 1 EasyCrypt pre-1.x

Status: reopened (2 matches)

Ticket Summary Owner Type Priority Component Version
#17182 Renaming internal symbols on cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17186 using [bypr] in odd way can result in badly formed goal Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
1 2 3 4 5 6
Note: See TracQuery for help on using queries.