Code

Subtyping proofs#415

Code

Open

crizkallah wants to merge 7 commits intomasterau-ts/cogent:masterfrom subtyping-proofsau-ts/cogent:subtyping-proofsCopy head branch name to clipboard

+331-74

Commits

Commits on Oct 18, 2019

• proofs: tmp work on subtyping theory

  vjackson725

  committed
  034ced5

  Copy full SHA for 034ced5

Commits on Oct 21, 2019

• proof of coherence of subsumption still needs proof of determinism of evaluation

  

  Christine Rizkallah

  committed
  2544f61

  Copy full SHA for 2544f61

• proofs: clear most cases in val_eval_deterministic

  vjackson725

  committed
  271586a

  Copy full SHA for 271586a

• val_eval_deterministic proof and therefore coherence_of_subsumption

  

  Christine Rizkallah

  committed
  600b1fa

  Copy full SHA for 600b1fa

• proofs: fix Correspondence

  vjackson725

  committed
  7174309

  Copy full SHA for 7174309

• proofs: fix Cogent_Corres

  vjackson725

  committed
  a4d944a

  Copy full SHA for a4d944a

Commits on Oct 28, 2019

• proofs: fix breakage in CorresProof due to missing simps in typetac

  vjackson725

  committed
  87b591c

  Copy full SHA for 87b591c