Code

Can call merge [Ignore]#6002

Code

Draft

typerSniper wants to merge 192 commits intodafny-lang:masterdafny-lang/dafny:masterfrom typerSniper:can-call-merge-boogaltyperSniper/dafny:can-call-merge-boogalCopy head branch name to clipboard

+1,122-694

Commits

Commits on Jun 11, 2024

• Snapshot changes

  RustanLeino

  committed
  e5e3e7c

  Copy full SHA for e5e3e7c

• Merge branch 'master' into can-call-diff

  Show description for 0ad2411
  RustanLeino

  committed
  0ad2411

  Copy full SHA for 0ad2411

• Fix parameter order to CanCallAssumption

  RustanLeino

  committed
  facdbef

  Copy full SHA for facdbef

• Manually merge in the changes from the old Translator.cs

  RustanLeino

  committed
  2cd6a52

  Copy full SHA for 2cd6a52

Commits on Jun 12, 2024

• Fix merge

  RustanLeino

  committed
  702c222

  Copy full SHA for 702c222

• Add FreeRequires/FreeEnsures helper methods

  RustanLeino

  committed
  86738d6

  Copy full SHA for 86738d6

• chore: Remove deprecated semi-colons

  RustanLeino

  committed
  e712995

  Copy full SHA for e712995

• Restore FunctionSpecification.dfy

  RustanLeino

  committed
  bf0ec2c

  Copy full SHA for bf0ec2c

• Move generation of req==>CanCall axiom

  RustanLeino

  committed
  73d0b5c

  Copy full SHA for 73d0b5c

• Replace kv parameter by alwaysAssume option in Free-Requires/Ensures

  RustanLeino

  committed
  13aa0d9

  Copy full SHA for 13aa0d9

• Don’t add CanCall _inside_ frame condition, but as free precondition

  RustanLeino

  committed
  e7e6c61

  Copy full SHA for e7e6c61

Commits on Jun 13, 2024

• Assume CanCall of callee frames

  RustanLeino

  committed
  e1e695b

  Copy full SHA for e1e695b

• chore: Remove deprecated semi-colons

  RustanLeino

  committed
  500ff5c

  Copy full SHA for 500ff5c

Commits on Jun 14, 2024

• Generate CanCall assumptions for result of calc

  RustanLeino

  committed
  79d3291

  Copy full SHA for 79d3291

Commits on Jun 17, 2024

• Generate CanCall assumptions for array/seq init expression

  RustanLeino

  committed
  ecef1e7

  Copy full SHA for ecef1e7

• Carve pre/post-conditions up into separate conjuncts

  Show description for 8f5822f
  RustanLeino

  committed
  8f5822f

  Copy full SHA for 8f5822f

Commits on Jun 20, 2024

• Fix null dereference

  RustanLeino

  committed
  5e697d2

  Copy full SHA for 5e697d2

• chore: Remove stale comment

  RustanLeino

  committed
  8cc0ba6

  Copy full SHA for 8cc0ba6

Commits on Jul 16, 2024

• Strip any box/unbox around trigger terms

  RustanLeino

  committed
  8f0b321

  Copy full SHA for 8f0b321

• Fix casts in test case

  RustanLeino

  committed
  2dc5fa4

  Copy full SHA for 2dc5fa4

• Fix ConjunctsOf to not drop labels

  RustanLeino

  committed
  ea774a5

  Copy full SHA for ea774a5

• Add CanCalls to primed version of comprehension uniqueness check

  RustanLeino

  committed
  466c1b8

  Copy full SHA for 466c1b8

• Reflect change in error output ordering

  RustanLeino

  committed
  171939e

  Copy full SHA for 171939e

• Fix Conjuncts all to include type of new LetExpr’s

  RustanLeino

  committed
  c7222b6

  Copy full SHA for c7222b6

• Add CanCall assumptions to subset-constraint checks

  RustanLeino

  committed
  94a0ccc

  Copy full SHA for 94a0ccc

Commits on Jul 17, 2024

• Restructure CanCallOptions and make allowances for overriding functions

  RustanLeino

  committed
  f059ffd

  Copy full SHA for f059ffd

• Add CanCan antecedent to “r” component of function handles

  RustanLeino

  committed
  d63ff0a

  Copy full SHA for d63ff0a

Commits on Jul 20, 2024

• Remove deprecation

  RustanLeino

  committed
  f7bf313

  Copy full SHA for f7bf313

• Use :induction instead of /induction:3

  RustanLeino

  committed
  460e400

  Copy full SHA for 460e400

• Add CanCall assumptions to generated let function

  Show description for 09be550
  RustanLeino

  committed
  09be550

  Copy full SHA for 09be550

• Adjust test case, which is now passing

  RustanLeino

  committed
  87b6f0f

  Copy full SHA for 87b6f0f

Commits on Jul 22, 2024

• Incorporate CanCall into newtype/subset-type $Is axioms

  Show description for 3127da2
  RustanLeino

  committed
  3127da2

  Copy full SHA for 3127da2

• Update order of error messages in expect file

  RustanLeino

  committed
  8bba9a1

  Copy full SHA for 8bba9a1

• Remove a redundant test file

  RustanLeino

  committed
  567c667

  Copy full SHA for 567c667

• Adjust test output

  RustanLeino

  committed
  7db4ffc

  Copy full SHA for 7db4ffc

• Fix parameters to CanCall function in override axiom

  RustanLeino

  committed
  e5c91dd

  Copy full SHA for e5c91dd

Commits on Jul 23, 2024

• Change override axiom to use CanCall

  RustanLeino

  committed
  1379380

  Copy full SHA for 1379380

• Adjust resource limit (down) to make test pass

  RustanLeino

  committed
  3a8307e

  Copy full SHA for 3a8307e

Commits on Jul 30, 2024

• Fix typo in comments

  RustanLeino

  committed
  a9b195a

  Copy full SHA for a9b195a

• Add workaround for incorrect partial-arrow constraint

  RustanLeino

  committed
  afdb5c5

  Copy full SHA for afdb5c5

• Merge branch 'master' into can-call-everywhere

  Show description for b657928
  RustanLeino

  committed
  b657928

  Copy full SHA for b657928

Commits on Sep 27, 2024

• Merge branch 'master' into can-call-everywhere

  Show description for 1cb2672
  RustanLeino

  committed
  1cb2672

  Copy full SHA for 1cb2672

• Merge branch 'master' into can-call-everywhere

  RustanLeino

  committed
  bcc497b

  Copy full SHA for bcc497b

Commits on Sep 30, 2024

• update resource count, this is positive

  typerSniper

  committed
  6a1b106

  Copy full SHA for 6a1b106

Commits on Oct 3, 2024

• Fix bad refactoring

  RustanLeino

  committed
  349a2ea

  Copy full SHA for 349a2ea

• Adjust test and answer

  RustanLeino

  committed
  5cee693

  Copy full SHA for 5cee693

• Add CanCall assumptions in short-circuit WF-result checks

  Show description for 0a45814
  RustanLeino

  committed
  0a45814

  Copy full SHA for 0a45814

• Fix implementations of Disjuncts and Conjuncts

  RustanLeino

  committed
  8973a0a

  Copy full SHA for 8973a0a

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  74fb993

  Copy full SHA for 74fb993

• Change \d to [0-9], since the former apparently isn’t always supported

  RustanLeino

  committed
  9ec69b2

  Copy full SHA for 9ec69b2

Commits on Oct 4, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  760fbe7

  Copy full SHA for 760fbe7

• Merge branch 'master' into can-call-everywhere

  RustanLeino

  committed
  ceff013

  Copy full SHA for ceff013

• Merge branch 'master' into can-call-everywhere

  RustanLeino

  committed
  f4c9588

  Copy full SHA for f4c9588

Commits on Oct 7, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  59f2e6f

  Copy full SHA for 59f2e6f

Commits on Oct 8, 2024

• Adjust test and answer

  Show description for d7a2754
  RustanLeino

  committed
  d7a2754

  Copy full SHA for d7a2754

Commits on Oct 9, 2024

• Avoid triggers with nullary functions

  Show description for b8332aa
  RustanLeino

  committed
  b8332aa

  Copy full SHA for b8332aa

• chore: Remove old syntax

  RustanLeino

  committed
  09b3930

  Copy full SHA for 09b3930

• Reorder error output

  RustanLeino

  committed
  96cd511

  Copy full SHA for 96cd511

• Update RUs in test outputs

  RustanLeino

  committed
  41fa183

  Copy full SHA for 41fa183

Commits on Oct 10, 2024

• merge

  typerSniper

  committed
  3927069

  Copy full SHA for 3927069

• Separate assertions into separate methods to avoid Z3 ordering problem

  RustanLeino

  committed
  522513f

  Copy full SHA for 522513f

Commits on Oct 12, 2024

• chore: Improve trigger/induction code

  RustanLeino

  committed
  5f3cfdc

  Copy full SHA for 5f3cfdc

• Compute triggers for automatic induction

  RustanLeino

  committed
  cd9d205

  Copy full SHA for cd9d205

• chore: Improve trigger/induction code

  Show description for 8c4c4a6
  RustanLeino

  committed
  8c4c4a6

  Copy full SHA for 8c4c4a6

• Compute triggers for automatic induction

  Show description for e62d2b6
  RustanLeino

  committed
  e62d2b6

  Copy full SHA for e62d2b6

• Improve induction heuristics

  RustanLeino

  committed
  ad1c724

  Copy full SHA for ad1c724

• chore: Change “ghost method” to “lemma”

  RustanLeino

  committed
  29d715a

  Copy full SHA for 29d715a

Commits on Oct 14, 2024

• chore: Improve C#

  RustanLeino

  committed
  4cfbe21

  Copy full SHA for 4cfbe21

• Also consider codatatype equality as a greatest focal predicate

  RustanLeino

  committed
  b17c662

  Copy full SHA for b17c662

• Show tooltips for any quantifier rewrite substitutions

  RustanLeino

  committed
  cee8d58

  Copy full SHA for cee8d58

• feat!: Auto-induction for twostate lemmas but not ghost methods

  RustanLeino

  committed
  dda37cb

  Copy full SHA for dda37cb

Commits on Oct 16, 2024

• fix: Don’t consider arrow-typed variables for auto induction

  RustanLeino

  committed
  fa79ba3

  Copy full SHA for fa79ba3

• feat: allow ternary expressions in triggers

  RustanLeino

  committed
  0028a3a

  Copy full SHA for 0028a3a

• Compute and use triggers for induction hypotheses

  RustanLeino

  committed
  394c635

  Copy full SHA for 394c635

• Tooltip named expressions from trigger selection

  RustanLeino

  committed
  659d4ba

  Copy full SHA for 659d4ba

• chore: Remove deprecated semi-colons

  RustanLeino

  committed
  6b5b207

  Copy full SHA for 6b5b207

• Add tests for ternary expressions in triggers

  RustanLeino

  committed
  3fc56d3

  Copy full SHA for 3fc56d3

• Adjust resource count in test

  RustanLeino

  committed
  73d2d61

  Copy full SHA for 73d2d61

• Merge branch 'master' into triggers-for-auto-induction

  RustanLeino

  committed
  73406c6

  Copy full SHA for 73406c6

• Add release notes

  RustanLeino

  committed
  f4815f4

  Copy full SHA for f4815f4

Commits on Oct 17, 2024

• Help proof

  RustanLeino

  committed
  e4e4ce8

  Copy full SHA for e4e4ce8

• Update test, which no longer exhausts resources

  RustanLeino

  committed
  3a0f1c0

  Copy full SHA for 3a0f1c0

• Improve proofs

  RustanLeino

  committed
  703c661

  Copy full SHA for 703c661

Commits on Oct 18, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  73b5ee9

  Copy full SHA for 73b5ee9

• Merge remote-tracking branch 'origin/master' into can-call-everywhere

  keyboardDrummer

  committed
  8547807

  Copy full SHA for 8547807

• Merge remote-tracking branch 'origin/master' into can-call-everywhere

  keyboardDrummer

  committed
  c164820

  Copy full SHA for c164820

Commits on Oct 19, 2024

• Improve induction heuristics

  RustanLeino

  committed
  9c07f8a

  Copy full SHA for 9c07f8a

• chore: Change “ghost method” to “lemma”

  RustanLeino

  committed
  a420bc2

  Copy full SHA for a420bc2

• chore: Improve C#

  RustanLeino

  committed
  2f9a6e1

  Copy full SHA for 2f9a6e1

• Also consider codatatype equality as a greatest focal predicate

  RustanLeino

  committed
  d6bc12e

  Copy full SHA for d6bc12e

• Show tooltips for any quantifier rewrite substitutions

  RustanLeino

  committed
  cb0eebd

  Copy full SHA for cb0eebd

• feat!: Auto-induction for twostate lemmas but not ghost methods

  RustanLeino

  committed
  2c4d9bc

  Copy full SHA for 2c4d9bc

• fix: Don’t consider arrow-typed variables for auto induction

  RustanLeino

  committed
  5b83dfa

  Copy full SHA for 5b83dfa

• feat: allow ternary expressions in triggers

  RustanLeino

  committed
  f26466b

  Copy full SHA for f26466b

• Compute and use triggers for induction hypotheses

  Show description for 6b4ca54
  RustanLeino

  committed
  6b4ca54

  Copy full SHA for 6b4ca54

• Tooltip named expressions from trigger selection

  RustanLeino

  committed
  bc050cd

  Copy full SHA for bc050cd

• chore: Remove deprecated semi-colons

  RustanLeino

  committed
  b9083e7

  Copy full SHA for b9083e7

• Add tests for ternary expressions in triggers

  RustanLeino

  committed
  a2b5a6f

  Copy full SHA for a2b5a6f

Commits on Oct 20, 2024

• Selectively exclude CanCalls from forall stmt translation

  RustanLeino

  committed
  84bd747

  Copy full SHA for 84bd747

• Fix typo in method name

  RustanLeino

  committed
  54e9ddb

  Copy full SHA for 54e9ddb

• Remove unnecessary assertion

  RustanLeino

  committed
  b46f0dc

  Copy full SHA for b46f0dc

• Remove unnecessary $’s

  RustanLeino

  committed
  022685c

  Copy full SHA for 022685c

• Improve C# and comments

  RustanLeino

  committed
  4cb3f5a

  Copy full SHA for 4cb3f5a

• Revert tooltip printing of trigger named expressions

  RustanLeino

  committed
  a213285

  Copy full SHA for a213285

• Improve and document methods that compute/report induction triggers

  RustanLeino

  committed
  72c15fe

  Copy full SHA for 72c15fe

• Incomplete attempt at specifying behavior

  RustanLeino

  committed
  704af8c

  Copy full SHA for 704af8c

Commits on Oct 23, 2024

• doc: Align :induction documentation with actual behavior

  Show description for 9e9dd80
  cpitclaudel

  committed
  9e9dd80

  Copy full SHA for 9e9dd80

• Remove unnecessary $s

  cpitclaudel

  committed
  8a792b1

  Copy full SHA for 8a792b1

Commits on Oct 24, 2024

• Move :inductionPattern attribute generation to ComputeInductionTriggers

  Show description for 7c6ab84
  cpitclaudel

  committed
  7c6ab84

  Copy full SHA for 7c6ab84

• Allow users to disable trigger generation with an empty inductionTrigger

  cpitclaudel

  committed
  766ac5b

  Copy full SHA for 766ac5b

• Update documentation

  Show description for a3702d2
  cpitclaudel

  committed
  a3702d2

  Copy full SHA for a3702d2

• Add one more test for induction triggers

  cpitclaudel

  committed
  ffe54af

  Copy full SHA for ffe54af

• Document {:inductionTrigger}

  cpitclaudel

  committed
  8c7b06c

  Copy full SHA for 8c7b06c

Commits on Oct 25, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  4c1269a

  Copy full SHA for 4c1269a

Commits on Oct 28, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  24aa393

  Copy full SHA for 24aa393

Commits on Oct 30, 2024

• Always report “inductionTrigger”, not just in DEBUG build

  RustanLeino

  committed
  769d6cd

  Copy full SHA for 769d6cd

• Fix format of expected test output

  RustanLeino

  committed
  2c7fcc9

  Copy full SHA for 2c7fcc9

• Merge branch 'master' into triggers-for-auto-induction

  Show description for 62e771c
  RustanLeino

  committed
  62e771c

  Copy full SHA for 62e771c

Commits on Oct 31, 2024

• Use underscore name for generated attributes

  Show description for af0223b
  RustanLeino

  committed
  af0223b

  Copy full SHA for af0223b

• Update tests

  RustanLeino

  committed
  6cdaa08

  Copy full SHA for 6cdaa08

• Update tests and expected output

  RustanLeino

  committed
  a1149c9

  Copy full SHA for a1149c9

• Fix previous code edit

  RustanLeino

  committed
  c447ffa

  Copy full SHA for c447ffa

• Merge branch 'master' into triggers-for-auto-induction

  RustanLeino

  committed
  3d8d0e7

  Copy full SHA for 3d8d0e7

• Update standard libraries

  RustanLeino

  committed
  63683d1

  Copy full SHA for 63683d1

• Merge branch 'master' into triggers-for-auto-induction

  RustanLeino

  committed
  808a2b3

  Copy full SHA for 808a2b3

• Merge branch 'master' into triggers-for-auto-induction

  Show description for 43bdbd3
  RustanLeino

  committed
  43bdbd3

  Copy full SHA for 43bdbd3

• Update standard library

  RustanLeino

  committed
  3652ff3

  Copy full SHA for 3652ff3

Commits on Nov 1, 2024

• Update standard library

  RustanLeino

  committed
  b070751

  Copy full SHA for b070751

Commits on Nov 5, 2024

• Merge branch 'triggers-for-auto-induction' into can-call-everywhere

  Show description for a56f5f6
  RustanLeino

  committed
  a56f5f6

  Copy full SHA for a56f5f6

Commits on Nov 6, 2024

• Merge branch 'master' into can-call-everywhere

  RustanLeino

  committed
  2e85691

  Copy full SHA for 2e85691

• Fix merge

  RustanLeino

  committed
  99f1c6e

  Copy full SHA for 99f1c6e

• Merge branch 'master' into can-call-everywhere

  Show description for 4bd711e
  RustanLeino

  committed
  4bd711e

  Copy full SHA for 4bd711e

Commits on Nov 7, 2024

• Merge branch 'master' into can-call-everywhere

  RustanLeino

  committed
  3086933

  Copy full SHA for 3086933

• Fix proof

  RustanLeino

  committed
  f3e2616

  Copy full SHA for f3e2616

• Use $OneHeap in Apply if function is known to be heap independent

  Show description for f94ccd2
  RustanLeino

  committed
  f94ccd2

  Copy full SHA for f94ccd2

Commits on Nov 11, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  96d69a7

  Copy full SHA for 96d69a7

• upd rc

  typerSniper

  committed
  1d247d1

  Copy full SHA for 1d247d1

• fuel expect upadte

  typerSniper

  committed
  e3dbc66

  Copy full SHA for e3dbc66

• update rc

  typerSniper

  committed
  e3b27ed

  Copy full SHA for e3b27ed

• Merge branch 'master' into can-call-everywhere

  Show description for 5947deb
  RustanLeino

  committed
  5947deb

  Copy full SHA for 5947deb

• merge

  typerSniper

  committed
  53bc59b

  Copy full SHA for 53bc59b

• Update BoogieGenerator.Methods.cs

  Show description for 756ceb6
  typerSniper

  authored
  756ceb6

  Copy full SHA for 756ceb6

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  596da12

  Copy full SHA for 596da12

• rc

  typerSniper

  committed
  f802e72

  Copy full SHA for f802e72

Commits on Nov 18, 2024

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  83213eb

  Copy full SHA for 83213eb

• expect updf

  typerSniper

  committed
  0409d51

  Copy full SHA for 0409d51

• fix heap picked for seq#create

  typerSniper

  committed
  3dfd94c

  Copy full SHA for 3dfd94c

• use oneheap for sequence intiailer

  typerSniper

  committed
  99fc5c1

  Copy full SHA for 99fc5c1

• fix old the heap used inside lambda body

  typerSniper

  committed
  96bdb79

  Copy full SHA for 96bdb79

Commits on Nov 20, 2024

• help verifier

  typerSniper

  committed
  21f43ed

  Copy full SHA for 21f43ed

• fighting butterflies with butterflies

  typerSniper

  committed
  3cd8cf5

  Copy full SHA for 3cd8cf5

• temp undo

  typerSniper

  committed
  92b21e4

  Copy full SHA for 92b21e4

• gcd

  typerSniper

  committed
  d1db55e

  Copy full SHA for d1db55e

• num ver

  typerSniper

  committed
  165065e

  Copy full SHA for 165065e

Commits on Nov 25, 2024

• try isolate

  typerSniper

  committed
  8330d54

  Copy full SHA for 8330d54

• null based heaping

  typerSniper

  committed
  f24e931

  Copy full SHA for f24e931

• typo

  typerSniper

  committed
  2edf581

  Copy full SHA for 2edf581

• finalize heap change for lambads

  typerSniper

  committed
  f266ad7

  Copy full SHA for f266ad7

• change trigger on requires to only depend on heap mentions in the spec

  typerSniper

  committed
  8ae7880

  Copy full SHA for 8ae7880

• split assertions into two methods

  typerSniper

  committed
  b23d1d3

  Copy full SHA for b23d1d3

• eof

  typerSniper

  committed
  6fc4bd1

  Copy full SHA for 6fc4bd1

• update resources

  typerSniper

  committed
  7131311

  Copy full SHA for 7131311

• upd fuel leg

  typerSniper

  committed
  7040b1f

  Copy full SHA for 7040b1f

Commits on Nov 26, 2024

• upd both

  typerSniper

  committed
  700d2a6

  Copy full SHA for 700d2a6

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  c6a1d8b

  Copy full SHA for c6a1d8b

Commits on Nov 27, 2024

• Update proof

  RustanLeino

  committed
  179d8e8

  Copy full SHA for 179d8e8

Commits on Nov 29, 2024

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  8d55b67

  Copy full SHA for 8d55b67

Commits on Dec 2, 2024

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  d5bd1f4

  Copy full SHA for d5bd1f4

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  8753d27

  Copy full SHA for 8753d27

• Update expected coverage output

  RustanLeino

  committed
  d302167

  Copy full SHA for d302167

• Update expected resource counts

  RustanLeino

  committed
  28452b0

  Copy full SHA for 28452b0

Commits on Dec 3, 2024

• Update coverage output

  RustanLeino

  committed
  2d3cf69

  Copy full SHA for 2d3cf69

• Fix typos in test harness

  RustanLeino

  committed
  2006f98

  Copy full SHA for 2006f98

• Update coverage output further

  RustanLeino

  committed
  b0ca029

  Copy full SHA for b0ca029

Commits on Dec 12, 2024

• Merge branch 'master' of https://github.com/dafny-lang/dafny into can-call-merge

  Show description for 6d9e3cf
  typerSniper

  committed
  6d9e3cf

  Copy full SHA for 6d9e3cf

• forgot

  typerSniper

  committed
  641320f

  Copy full SHA for 641320f

• update thsoe agains

  typerSniper

  committed
  b7f7dd1

  Copy full SHA for b7f7dd1

• update rc

  typerSniper

  committed
  719a9d3

  Copy full SHA for 719a9d3

• Merge branch 'master' of https://github.com/dafny-lang/dafny into can-call-merge

  typerSniper

  committed
  432ea9a

  Copy full SHA for 432ea9a

Commits on Dec 16, 2024

• nc to pc is okay

  typerSniper

  committed
  2e4b4a5

  Copy full SHA for 2e4b4a5

• update rc

  typerSniper

  committed
  b88a8b2

  Copy full SHA for b88a8b2

• Merge branch 'master' of https://github.com/dafny-lang/dafny into can-call-merge

  Show description for cc2e79d
  typerSniper

  committed
  cc2e79d

  Copy full SHA for cc2e79d

• merge with master wagain

  typerSniper

  committed
  2ee1347

  Copy full SHA for 2ee1347

• update limited expet

  typerSniper

  committed
  313383c

  Copy full SHA for 313383c

Commits on Dec 17, 2024

• read conditions update

  typerSniper

  committed
  6b1df08

  Copy full SHA for 6b1df08

• space changes

  typerSniper

  committed
  500216f

  Copy full SHA for 500216f

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  c39a975

  Copy full SHA for c39a975

Commits on Dec 18, 2024

• Merge branch 'master' into can-call-everywhere

  typerSniper

  authored
  913959a

  Copy full SHA for 913959a

• Merge branch 'master' of https://github.com/dafny-lang/dafny into can-call-everywhere

  typerSniper

  committed
  460dcd1

  Copy full SHA for 460dcd1

Commits on Dec 23, 2024

• Merge branch 'can-call-everywhere' of https://github.com/RustanLeino/dafny into can-call-everywhere

  typerSniper

  committed
  d173e1f

  Copy full SHA for d173e1f

• Merge branch 'master' of https://github.com/dafny-lang/dafny into can-call-everywhere

  Show description for ac574be
  typerSniper

  committed
  ac574be

  Copy full SHA for ac574be

• merge

  typerSniper

  committed
  2c7d72b

  Copy full SHA for 2c7d72b