Code

Coq: Add vec#154

Code

Closed

nomeata wants to merge 27 commits intomasterdfinity/candid:masterfrom joachim/coq-vecdfinity/candid:joachim/coq-vecCopy head branch name to clipboard

+1,027-20

Commits

Commits on Nov 30, 2020

• Empty Coq setup

  Show description for 08c220e
  nomeata

  committed
  08c220e

  Copy full SHA for 08c220e

• Formalize IDL-Soundness

  Show description for fcaeaa1
  nomeata

  committed
  fcaeaa1

  Copy full SHA for fcaeaa1

• Try to add CI

  nomeata

  committed
  f2a1868

  Copy full SHA for f2a1868

Commits on Dec 1, 2020

• State assumptions of soundness proof

  nomeata

  committed
  29e29d5

  Copy full SHA for 29e29d5

• Outline some of the proof

  nomeata

  committed
  e963b0b

  Copy full SHA for e963b0b

Commits on Dec 3, 2020

• Finish IDL-Soundess proof

  nomeata

  committed
  f1dd58f

  Copy full SHA for f1dd58f

• Small cleanup

  nomeata

  committed
  88551a3

  Copy full SHA for 88551a3

• Coq: MiniCandid

  Show description for b5ca271
  nomeata

  committed
  b5ca271

  Copy full SHA for b5ca271

• Show that is_not_opt_like_type t <-> ~ (NullT <: t)

  nomeata

  committed
  0f7a326

  Copy full SHA for 0f7a326

Commits on Dec 4, 2020

• Merge branch 'master' of github.com:dfinity/candid into joachim/coq-candid

  nomeata

  committed
  ab7f474

  Copy full SHA for ab7f474

• Play around with named cases

  nomeata

  committed
  40f45ab

  Copy full SHA for 40f45ab

• Add VoidT

  nomeata

  committed
  d1d72b1

  Copy full SHA for d1d72b1

• Add ReservedT

  nomeata

  committed
  091c951

  Copy full SHA for 091c951

• Make named_constructor more strict

  nomeata

  committed
  614b112

  Copy full SHA for 614b112

• Simplify

  nomeata

  committed
  f50f0de

  Copy full SHA for f50f0de

• Prettier case names

  nomeata

  committed
  ebd6081

  Copy full SHA for ebd6081

Commits on Dec 5, 2020

• A little bit of cleanup

  nomeata

  committed
  1ee3044

  Copy full SHA for 1ee3044

• Use NamedCases in IDLSoundness

  nomeata

  committed
  5ffd78d

  Copy full SHA for 5ffd78d

Commits on Dec 9, 2020

• Towards the opportunistic subtyping

  nomeata

  committed
  db700e2

  Copy full SHA for db700e2

Commits on Dec 10, 2020

• Conclude the proof for opportunistic decoding

  nomeata

  committed
  e8f24ee

  Copy full SHA for e8f24ee

Commits on Dec 11, 2020

• Move NamedCasesDemo into own file

  nomeata

  committed
  9c8d3fd

  Copy full SHA for 9c8d3fd

• Wrap up the proofs

  nomeata

  committed
  72cb55c

  Copy full SHA for 72cb55c

• Introduce does-not-coerce relation

  nomeata

  committed
  458551d

  Copy full SHA for 458551d

• Merge branch 'master' into joachim/coq-candid

  nomeata

  authored
  d9ce594

  Copy full SHA for d9ce594

• Use does-not-coerce relation more

  nomeata

  committed
  2d9af91

  Copy full SHA for 2d9af91

• Simpler, faster tactics

  nomeata

  committed
  13595fd

  Copy full SHA for 13595fd

Commits on Dec 20, 2020

• Coq: Add vec

  Show description for 419a7a5
  nomeata

  committed
  419a7a5

  Copy full SHA for 419a7a5