Code

Prove subtyping case for soundness#153

Code

Merged

Ailrun merged 8 commits intomainBeluga-lang/McTT:mainfrom pr-subtyping-lemmasBeluga-lang/McTT:pr-subtyping-lemmasCopy head branch name to clipboardAug 15, 2024

+397-102

Commits

Commits on Aug 8, 2024

• Prove subtyping lemma

  Ailrun

  committed
  6656625

  Copy full SHA for 6656625

• Stuck

  Ailrun

  committed
  54ed0f2

  Copy full SHA for 54ed0f2

• Fix CI

  Ailrun

  committed
  ca00983

  Copy full SHA for ca00983

Commits on Aug 9, 2024

• Some updates

  Ailrun

  committed
  f382bd2

  Copy full SHA for f382bd2

Commits on Aug 11, 2024

• Prove subtyping case with some admitted asserts

  Ailrun

  committed
  e373087

  Copy full SHA for e373087

• Fix CI error

  Ailrun

  committed
  9093c95

  Copy full SHA for 9093c95

Commits on Aug 12, 2024

• Remove most of admitted subgoals

  Ailrun

  committed
  28e13a2

  Copy full SHA for 28e13a2

Commits on Aug 15, 2024

• Refactor proofs a bit

  Ailrun

  committed
  925106d

  Copy full SHA for 925106d