Code

v2.0#27

Code

Merged

aleksnanevski merged 97 commits intomasterimdea-software/htt:masterfrom v2.0imdea-software/htt:v2.0Copy head branch name to clipboardSep 30, 2024

+4,475-3,819

Commits

Commits on Aug 1, 2024

• blah

  aleksnanevski

  committed
  9c49b87

  Copy full SHA for 9c49b87

• adding files

  aleksnanevski

  committed
  b94f334

  Copy full SHA for b94f334

• renaming

  aleksnanevski

  committed
  c4ba78e

  Copy full SHA for c4ba78e

• blah

  aleksnanevski

  committed
  d0cf277

  Copy full SHA for d0cf277

• removed interlude.v

  aleksnanevski

  committed
  fd96996

  Copy full SHA for fd96996

• started refactoring model.v

  aleksnanevski

  committed
  b4d3053

  Copy full SHA for b4d3053

• minor

  aleksnanevski

  committed
  daf3122

  Copy full SHA for daf3122

Commits on Aug 2, 2024

• started refactoring examples

  aleksnanevski

  committed
  5af6420

  Copy full SHA for 5af6420

• continuing refactoring

  aleksnanevski

  committed
  cd47cf2

  Copy full SHA for cd47cf2

Commits on Aug 5, 2024

• refactored a bunch of examples.

  Show description for 5270a21
  aleksnanevski

  committed
  5270a21

  Copy full SHA for 5270a21

• started refactoring graph.v

  aleksnanevski

  committed
  23ce5ab

  Copy full SHA for 23ce5ab

• minor

  aleksnanevski

  committed
  2632e78

  Copy full SHA for 2632e78

• wip

  aleksnanevski

  committed
  7c38ffa

  Copy full SHA for 7c38ffa

Commits on Aug 6, 2024

• continuing with refactoring graph.v.

  aleksnanevski

  committed
  35b30ff

  Copy full SHA for 35b30ff

Commits on Aug 7, 2024

• blah

  aleksnanevski

  committed
  3c21f95

  Copy full SHA for 3c21f95

• blah

  aleksnanevski

  committed
  1058fcf

  Copy full SHA for 1058fcf

• blah

  aleksnanevski

  committed
  2394b9f

  Copy full SHA for 2394b9f

• comments about do we want to follow dangling edges to their

  Show description for 79baaaf
  aleksnanevski

  committed
  79baaaf

  Copy full SHA for 79baaaf

• comments

  aleksnanevski

  committed
  a99d04d

  Copy full SHA for a99d04d

• minor

  aleksnanevski

  committed
  ecdc4de

  Copy full SHA for ecdc4de

• minor

  aleksnanevski

  committed
  d24ddf0

  Copy full SHA for d24ddf0

Commits on Aug 8, 2024

• blah

  aleksnanevski

  committed
  443bd2e

  Copy full SHA for 443bd2e

• wip

  aleksnanevski

  committed
  f9a4eb5

  Copy full SHA for f9a4eb5

• wip

  aleksnanevski

  committed
  8944fd1

  Copy full SHA for 8944fd1

Commits on Aug 9, 2024

• refactored schorr.v

  aleksnanevski

  committed
  83aa06d

  Copy full SHA for 83aa06d

• committed schorr

  aleksnanevski

  committed
  7eb1ccf

  Copy full SHA for 7eb1ccf

• minor

  aleksnanevski

  committed
  bcd4158

  Copy full SHA for bcd4158

• minor

  aleksnanevski

  committed
  75722a2

  Copy full SHA for 75722a2

• minor

  aleksnanevski

  committed
  6b3c09d

  Copy full SHA for 6b3c09d

• minor

  aleksnanevski

  committed
  40ef923

  Copy full SHA for 40ef923

• moved some helper lemmas to seqext.v

  aleksnanevski

  committed
  e0c6c22

  Copy full SHA for e0c6c22

• blah

  aleksnanevski

  committed
  6ef5717

  Copy full SHA for 6ef5717

Commits on Aug 12, 2024

• blah

  aleksnanevski

  committed
  f030b03

  Copy full SHA for f030b03

• Merge branch 'master' of gitlab.software.imdea.org:aleks/hoare-type-theory

  aleksnanevski

  committed
  cc242ca

  Copy full SHA for cc242ca

• blah

  aleksnanevski

  committed
  ab837f6

  Copy full SHA for ab837f6

• blah

  aleksnanevski

  committed
  4db8d48

  Copy full SHA for 4db8d48

• blah

  aleksnanevski

  committed
  3cc4ffa

  Copy full SHA for 3cc4ffa

• blah

  aleksnanevski

  committed
  e666696

  Copy full SHA for e666696

• blah

  aleksnanevski

  committed
  b7bb9b9

  Copy full SHA for b7bb9b9

• blah

  aleksnanevski

  committed
  bb322d1

  Copy full SHA for bb322d1

• wip

  aleksnanevski

  committed
  f1e7cfe

  Copy full SHA for f1e7cfe

Commits on Aug 13, 2024

• some cleaning up in congprog.v

  aleksnanevski

  committed
  507f228

  Copy full SHA for 507f228

• cleanup in congprog.v

  aleksnanevski

  committed
  67088c5

  Copy full SHA for 67088c5

• cleanup

  aleksnanevski

  committed
  39d7b49

  Copy full SHA for 39d7b49

• cleanup

  aleksnanevski

  committed
  cc4be98

  Copy full SHA for cc4be98

• blah

  aleksnanevski

  committed
  db551c3

  Copy full SHA for db551c3

Commits on Aug 14, 2024

• ported proofs of congr_prog

  aleksnanevski

  committed
  2ff85e2

  Copy full SHA for 2ff85e2

• modified congprog to use postconditions with vfun.

  aleksnanevski

  committed
  55dfc75

  Copy full SHA for 55dfc75

• abstracting the code in congprog.v

  aleksnanevski

  committed
  cd96ba5

  Copy full SHA for cd96ba5

• defining shape predicate

  

  kevinlopez

  committed
  241fac7

  Copy full SHA for 241fac7

• wMerge branch 'kevin' of https://gitlab.software.imdea.org/aleks/hoare-type-theory into kevin

  

  kevinlopez

  committed
  91b6437

  Copy full SHA for 91b6437

• made abstract type of root pointers of arrays and kvmaps be small

  Show description for 230f0f7
  aleksnanevski

  committed
  230f0f7

  Copy full SHA for 230f0f7

• developed a number of lemmas about star.

  Show description for 5616c43
  aleksnanevski

  committed
  5616c43

  Copy full SHA for 5616c43

Commits on Aug 15, 2024

• defining shape predicate

  

  kevinlopez

  committed
  ab0b85c

  Copy full SHA for ab0b85c

• Merge branch 'master' of https://gitlab.software.imdea.org/aleks/hoare-type-theory into kevin

  

  kevinlopez

  committed
  642f9e0

  Copy full SHA for 642f9e0

• defining shape predicate

  

  kevinlopez

  committed
  295c20d

  Copy full SHA for 295c20d

• blah

  aleksnanevski

  committed
  4a62478

  Copy full SHA for 4a62478

Commits on Aug 16, 2024

• reorgainzation of pred.v prelude.v and consequences.

  Show description for 4f64d25
  aleksnanevski

  committed
  4f64d25

  Copy full SHA for 4f64d25

• Merge branch 'master' of gitlab.software.imdea.org:aleks/hoare-type-theory

  aleksnanevski

  committed
  6798fbf

  Copy full SHA for 6798fbf

• removed some files that shouldn't be here

  aleksnanevski

  committed
  0084f0a

  Copy full SHA for 0084f0a

• moved additional lemmas from individual files to fcsl-pcm.

  Show description for 323ccb9
  aleksnanevski

  committed
  323ccb9

  Copy full SHA for 323ccb9

• minor

  aleksnanevski

  committed
  77b76dc

  Copy full SHA for 77b76dc

• sectioning of congmath.v

  aleksnanevski

  committed
  6b9d585

  Copy full SHA for 6b9d585

• minor

  aleksnanevski

  committed
  50909d9

  Copy full SHA for 50909d9

• modifying comments

  aleksnanevski

  committed
  c7725aa

  Copy full SHA for c7725aa

Commits on Aug 27, 2024

• changed natmap to add view for last_val

  aleksnanevski

  committed
  fad9a80

  Copy full SHA for fad9a80

• hm

  aleksnanevski

  committed
  4fd5dc9

  Copy full SHA for 4fd5dc9

• removed extraneous lemmas from unionmap.v

  aleksnanevski

  committed
  4984d6d

  Copy full SHA for 4984d6d

• minor

  aleksnanevski

  committed
  74ad918

  Copy full SHA for 74ad918

Commits on Aug 28, 2024

• changed In_dom_umfilt lemma to use exists2 instead of exists.

  aleksnanevski

  committed
  7ac8e43

  Copy full SHA for 7ac8e43

• found a way to view "weird" lemmas in natmap.v as non-weird.

  Show description for 75bfd6b
  aleksnanevski

  committed
  75bfd6b

  Copy full SHA for 75bfd6b

• propagating changed to natmap.v from mathador

  aleksnanevski

  committed
  f01615c

  Copy full SHA for f01615c

Commits on Aug 29, 2024

• added alternative lemma for seq_lt irreflexivity, one that isn't

  Show description for b426ffe
  aleksnanevski

  committed
  b426ffe

  Copy full SHA for b426ffe

• renaming slt_irrN into sltnn

  aleksnanevski

  committed
  af748a8

  Copy full SHA for af748a8

• added validPt2 and domPt2

  aleksnanevski

  committed
  ef24ddc

  Copy full SHA for ef24ddc

Commits on Sep 4, 2024

• propagating changes from mathador

  aleksnanevski

  committed
  ebdc17c

  Copy full SHA for ebdc17c

• blah

  aleksnanevski

  committed
  bea4570

  Copy full SHA for bea4570

• ibalh

  aleksnanevski

  committed
  93cd997

  Copy full SHA for 93cd997

Commits on Sep 5, 2024

• blah

  aleksnanevski

  committed
  a45938b

  Copy full SHA for a45938b

• blah

  aleksnanevski

  committed
  1c9b614

  Copy full SHA for 1c9b614

• blah

  aleksnanevski

  committed
  a2283a8

  Copy full SHA for a2283a8

Commits on Sep 6, 2024

• many changes introduced to deal with graphs

  aleksnanevski

  committed
  48f54a2

  Copy full SHA for 48f54a2

Commits on Sep 17, 2024

• preparing for release

  aleksnanevski

  committed
  73ab034

  Copy full SHA for 73ab034

Commits on Sep 23, 2024

• removed files inheritted from fcsl-pcm

  aleksnanevski

  committed
  cbd2c96

  Copy full SHA for cbd2c96

• added Marcos to the list of authors

  aleksnanevski

  committed
  0c83825

  Copy full SHA for 0c83825

• regenerated .opam files from meta.yml

  aleksnanevski

  committed
  ae6f24f

  Copy full SHA for ae6f24f

• removed devcomments

  aleksnanevski

  committed
  7ecce21

  Copy full SHA for 7ecce21

• removed some lemmas that have recently been included into mathcomp

  aleksnanevski

  committed
  5113278

  Copy full SHA for 5113278

Commits on Sep 24, 2024

• regenerated htt/dune file

  aleksnanevski

  committed
  03220f8

  Copy full SHA for 03220f8

Commits on Sep 27, 2024

• playing with dune

  aleksnanevski

  committed
  be7aaa8

  Copy full SHA for be7aaa8

• playing with dune

  aleksnanevski

  committed
  3dfe5dc

  Copy full SHA for 3dfe5dc

• forgot some files

  aleksnanevski

  committed
  48f3a50

  Copy full SHA for 48f3a50

• blah

  aleksnanevski

  committed
  e0539fe

  Copy full SHA for e0539fe

• blah

  aleksnanevski

  committed
  83baf96

  Copy full SHA for 83baf96

• blah

  aleksnanevski

  committed
  9a80b15

  Copy full SHA for 9a80b15

• blah

  aleksnanevski

  committed
  d725c09

  Copy full SHA for d725c09

• changed mustache files

  aleksnanevski

  committed
  9068807

  Copy full SHA for 9068807