Skip to content
Snippets Groups Projects
Select Git revision
  • add-blocker-graph-debug
  • add-map-equal-value-keys
  • dotty-compat
  • fix-stainless-1135
  • github/fork/SolalPirelli/sp/minimizer
  • github/fork/jad-hamza/replaceFromSymbols-positions
  • github/fork/mario-bucev/more-instantiation
  • main default
  • refactor-parser
  • scala-2.12.13
  • scala-2.13
  • v1.1.5
  • v1.1.0
  • v1.0.2
  • v1.0.1
  • v1.0
16 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.019Aug1817161413121186327Jul2526252423242322232221201917141310962130Jun292625242322211918171612111032129May2726222120191813121187654329Apr28292827282726272625242322212017161514231Mar26231918109654 Author credit and section flattening for proofs DSL (neon).Annotate fill with @libraryUse full names to match against --functions. Display qualified names.Added List.fill to the library. Script to run regressionsAllow ANSI escape codes within ASCII helpersPut these files togetherAdds documentation about theorem proving in Leon and the proof DSL.Adds test case illustrating reasoning by implication.Adds test case illustrating non-wellfoundedness issues with proofs.Adds test case for proof DSL: exponential function (some tests fail).Adds test case for proof DSL: discrete measures.Updates/adds lemmas about lists.Adds DSL for proofs.Changes argument of '==>' to be by-name.Flatten & Simplify Solver APIbleUpdate to latest scala-smtlibImprovementsTests in different packagesMove this to regression testsImprovementsAll types are supported for pattern matchingMake this more readableTest unapply-synthesis interactionRefactor grammars out of synthesisPropagate tests down ADT splitsSort files, so that regression tests run in a reproducible mannerRework ExamplesBank, generate inputs for synthesisOne test per file compiledRemove debugDefine Printable for non-leon-treesGrammars have access to ctxUnify Split and FocusIntroduce model minimization/maximizationSolver-based enumeration of modelsImplement asInstanceOfRemove toString, rely on asString instead when printing stuffCorrectly parenthesize implicationspreserve annotation arguments in the ASTUpdate CODING_GUIDELINES.md