Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on May 19, 2017

• Added "witness" clauses to newtype and subset-type declarations. Resolution and verification are done, but the compilation support for these is still missing.

  Show description for fe15015
  

  Rustan Leino

  committed
  fe15015

  Copy full SHA for fe15015

Commits on Sep 22, 2016

• Added parsing, type checking (but not yet other resolution checks and verification) of two-state functions and two-state predicates

  

  RustanLeino

  committed
  fd05502

  Copy full SHA for fd05502

Commits on Sep 20, 2016

• Added "allocated" expressions, which say that the argument expression, which can be of any type,

  Show description for 431dd00
  

  Rustan Leino

  committed
  431dd00

  Copy full SHA for 431dd00

Commits on Sep 18, 2016

• Syntax highlight bitvector types

  

  RustanLeino

  committed
  b0089a2

  Copy full SHA for b0089a2

• Added "unchanged" predicates.

  Show description for 33c67a5
  

  RustanLeino

  committed
  33c67a5

  Copy full SHA for 33c67a5

Commits on Aug 24, 2016

• Introduced "assert ... by { ... }" statements

  

  Rustan Leino

  committed
  989d984

  Copy full SHA for 989d984

Commits on Aug 9, 2016

• Brave new attempt at eol normalization

  

  RustanLeino

  committed
  6d82360

  Copy full SHA for 6d82360

Commits on Jun 18, 2016

• Remove cursor in banner

  cpitclaudel

  committed
  05f873b

  Copy full SHA for 05f873b

• Add a bit of spacing to the banner

  cpitclaudel

  committed
  66bcaa0

  Copy full SHA for 66bcaa0

Commits on Aug 23, 2015

• Replace the Emacs mode files by a pointer to the boogie-friends repo.

  Show description for 88e5569
  cpitclaudel

  committed
  88e5569

  Copy full SHA for 88e5569

Commits on May 29, 2015

• Add an infinite set collection type.

  qunyanm

  committed
  05f1ef9

  Copy full SHA for 05f1ef9

Commits on May 12, 2015

• Fixed typo in the Dafny Emacs mode.

  nadia-polikarpova

  committed
  92a1889

  Copy full SHA for 92a1889

Commits on May 7, 2015

• Added inductive predicates

  

  Rustan Leino

  committed
  568f543

  Copy full SHA for 568f543

Commits on Apr 27, 2015

• added notice about vim-loves-dafny.

  mlr-msft

  committed
  646569d

  Copy full SHA for 646569d

Commits on Mar 8, 2015

• Added 'protected' keyword (syntax)

  

  Rustan Leino

  committed
  21a3ca0

  Copy full SHA for 21a3ca0

Commits on Feb 27, 2015

• Removed Util/VS2010 folder, which has been superseded by DafnyExtension years ago

  

  Rustan Leino

  committed
  c4132b3

  Copy full SHA for c4132b3

• Add imap keyword to VS/emacs/vim/latex files

  Chris-Hawblitzel

  committed
  9bab789

  Copy full SHA for 9bab789

Commits on Oct 21, 2014

• Added types "char" and "string" (the latter being a synonym for "seq<char>").

  Show description for 4d3f7e8
  

  Rustan Leino

  committed
  4d3f7e8

  Copy full SHA for 4d3f7e8

Commits on Oct 10, 2014

• Reformatting of emacs syntax file.

  

  Rustan Leino

  committed
  623d193

  Copy full SHA for 623d193

Commits on Aug 22, 2014

• Changed syntax of derived types to "newtype"

  Show description for 75b9b52
  

  Rustan Leino

  committed
  75b9b52

  Copy full SHA for 75b9b52

Commits on Jul 18, 2014

• added trait feature:

  Show description for 5da9e16
  

  Reza Ahmadi

  committed
  5da9e16

  Copy full SHA for 5da9e16

Commits on Jul 7, 2014

• Fixes to vim highlighting

  

  Dan Rosen

  committed
  eb94b83

  Copy full SHA for eb94b83

Commits on Apr 4, 2014

• Added "modify" statement.

  Show description for ae33832
  

  Rustan Leino

  committed
  ae33832

  Copy full SHA for ae33832

Commits on Mar 20, 2014

• Fixed typo in latex style file

  

  Rustan Leino

  committed
  0e6fea0

  Copy full SHA for 0e6fea0

Commits on Feb 24, 2014

• Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma")

  

  Rustan Leino

  committed
  7767d28

  Copy full SHA for 7767d28

Commits on Feb 14, 2014

• Syntax highlighting for reals

  

  Rustan Leino

  committed
  ca1fc79

  Copy full SHA for ca1fc79

Commits on Feb 13, 2014

• Increased space around "..." in latex style for Dafny.

  

  Rustan Leino

  committed
  7c43697

  Copy full SHA for 7c43697

Commits on Feb 11, 2014

• Italicize attributes in latex mode for Dafny

  

  Rustan Leino

  committed
  502fbe4

  Copy full SHA for 502fbe4

Commits on Dec 12, 2013

• Fixed emacs coloring to not color things that are only substrings of symbols

  Show description for e73e5da
  

  Bryan Parno

  committed
  e73e5da

  Copy full SHA for e73e5da

Commits on Dec 10, 2013

• Add support for the "include" keyword, which accepts a (possibly relative) path

  Show description for 623eb5e
  

  Bryan Parno

  committed
  623eb5e

  Copy full SHA for 623eb5e

Commits on Aug 7, 2013

• Removed old keyword "choose"

  

  Rustan Leino

  committed
  2b19a9b

  Copy full SHA for 2b19a9b

Commits on Aug 3, 2013

• Introduced keywords "lemma" (like a "ghost method", but not allowed to have a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)

  

  Rustan Leino

  committed
  7a10653

  Copy full SHA for 7a10653

Commits on May 13, 2013

• Include <== operator in LaTeX style file

  

  Rustan Leino

  committed
  52eba18

  Copy full SHA for 52eba18

Commits on Mar 6, 2013

• Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional.

  

  Rustan Leino

  committed
  d2daea8

  Copy full SHA for d2daea8

Commits on Oct 22, 2012

• removed deprecated "allocated" keyword from DafnyExtension syntax highlighting

  Show description for ca21c2c
  

  Rustan Leino

  committed
  ca21c2c

  Copy full SHA for ca21c2c

Pagination

Previous

Next