Code

User-defined rewrite rules#50

Code

Open

TheoWinterhalter wants to merge 16 commits intocoq:mastercoq/rfcs:masterfrom CoqHott:rewCoqHott/ceps:rewCopy head branch name to clipboard

+202

Commits

Commits on Nov 24, 2020

• Skeleton for rewrite rules

  SkySkimmer

  committed
  06db1d4

  Copy full SHA for 06db1d4

Commits on Nov 25, 2020

• Detail rewrite rules CEP

  TheoWinterhalter

  committed
  eb7367b

  Copy full SHA for eb7367b

Commits on Nov 26, 2020

• Add application of pattern variables to bound variables

  TheoWinterhalter

  committed
  c3c0be7

  Copy full SHA for c3c0be7

• more examples, add url to POPL'21 paper

  tabareau

  committed
  582ec21

  Copy full SHA for 582ec21

• fix space

  tabareau

  committed
  df65b1c

  Copy full SHA for df65b1c

• Remove "..." in pattern syntax

  TheoWinterhalter

  committed
  56fea7a

  Copy full SHA for 56fea7a

• typo

  SkySkimmer

  committed
  c16fd70

  Copy full SHA for c16fd70

• Add forced patterns

  TheoWinterhalter

  committed
  c763217

  Copy full SHA for c763217

Commits on Nov 27, 2020

• add type-forced and precise type constructor

  tabareau

  committed
  e7ebf70

  Copy full SHA for e7ebf70

• Precise what type-forced mean

  TheoWinterhalter

  committed
  7750481

  Copy full SHA for 7750481

• Move ref out of the text

  TheoWinterhalter

  committed
  5048174

  Copy full SHA for 5048174

Commits on Nov 30, 2020

• remove mention of definitions as symbols

  tabareau

  committed
  cf5406b

  Copy full SHA for cf5406b

• Merge branch 'rew' of https://github.com/CoqHott/ceps into rew

  tabareau

  committed
  af5dffa

  Copy full SHA for af5dffa

Commits on Dec 3, 2020

• More detailed syntax and examples

  TheoWinterhalter

  committed
  a0b04d7

  Copy full SHA for a0b04d7

• Add examples

  TheoWinterhalter

  committed
  2fd637a

  Copy full SHA for 2fd637a

Commits on Jan 6, 2021

• typo

  tabareau

  authored
  e453b31

  Copy full SHA for e453b31