Code

Constructor & case type-checking#26

Code

Merged

liesnikov merged 25 commits intomainjespercockx/agda-core:mainfrom constructor-type-checkingjespercockx/agda-core:constructor-type-checkingCopy head branch name to clipboardApr 19, 2024

+408-142

Commits

Commits on Apr 17, 2024

• factor out elim-view reduction

  liesnikov

  committed
  4cc333c

  Copy full SHA for 4cc333c

• move checkCoerce out of the mutual block

  liesnikov

  committed
  80b44fc

  Copy full SHA for 80b44fc

• add a stub for constructor type-checking

  liesnikov

  committed
  8338ed0

  Copy full SHA for 8338ed0

• a stub for type-checking substitutions

  Show description for b029ba9
  liesnikov

  committed
  b029ba9

  Copy full SHA for b029ba9

• fix type-checking of substitutions

  liesnikov

  committed
  cb72e97

  Copy full SHA for cb72e97

• add a rough sketch of constructor typechecking

  liesnikov

  committed
  c1328a8

  Copy full SHA for c1328a8

• add a function with equality of args to match on in bind

  liesnikov

  committed
  9d1fa29

  Copy full SHA for 9d1fa29

• switch to a getConstructor version that returns an index and a proof

  Show description for 752aa96
  liesnikov

  committed
  752aa96

  Copy full SHA for 752aa96

• use nicer syntax in convsubst

  liesnikov

  committed
  8a15fcb

  Copy full SHA for 8a15fcb

• remove new interface files directory when cleaning

  liesnikov

  committed
  b6a385e

  Copy full SHA for b6a385e

• add a stub for branch type-checking

  liesnikov

  committed
  fdd939e

  Copy full SHA for fdd939e

• now missing only the motive and indices in the case type-checking

  liesnikov

  committed
  46ec10c

  Copy full SHA for 46ec10c

• fill in checkBranch

  liesnikov

  committed
  1e5d39c

  Copy full SHA for 1e5d39c

• add compile pragmas

  Show description for 3fca4bc
  liesnikov

  committed
  3fca4bc

  Copy full SHA for 3fca4bc

• handle indices when typechecking case

  liesnikov

  committed
  4ce6d1c

  Copy full SHA for 4ce6d1c

• add a stub for conversion of branches

  liesnikov

  committed
  75e3ef4

  Copy full SHA for 75e3ef4

• fix spacing in the inferElim

  liesnikov

  committed
  ccbc65f

  Copy full SHA for ccbc65f

• make things right(er)

  liesnikov

  committed
  6ce499c

  Copy full SHA for 6ce499c

• bump scope library version

  liesnikov

  committed
  a86c6b3

  Copy full SHA for a86c6b3

• cosmetics

  liesnikov

  committed
  58b62d1

  Copy full SHA for 58b62d1

• introduce motive in the syntax for cases

  Show description for 6b02481
  liesnikov

  committed
  6b02481

  Copy full SHA for 6b02481

Commits on Apr 19, 2024

• fill in the sort of the datatype in the conversion checking of elims

  liesnikov

  committed
  12d4bce

  Copy full SHA for 12d4bce

• add the case for conversion-inference of two pis

  liesnikov

  committed
  a002556

  Copy full SHA for a002556

• comments, whitespaces, and error messages

  liesnikov

  committed
  d75a500

  Copy full SHA for d75a500

• implement cases for Ann

  liesnikov

  committed
  0cb66d1

  Copy full SHA for 0cb66d1