Code

RFC: const-dependent type system.#1657

Code

Closed

ticki wants to merge 36 commits intorust-lang:masterrust-lang/rfcs:masterfrom ticki:pi-typesticki/rfcs:pi-typesCopy head branch name to clipboard

+1,139

Commits

Commits on Jun 22, 2016

• rfc: Π-types

  ticki

  committed
  27c33a3

  Copy full SHA for 27c33a3

• Expand the overview section

  ticki

  committed
  e4446c5

  Copy full SHA for e4446c5

• Propose alternative syntaxes

  ticki

  committed
  eb60cd3

  Copy full SHA for eb60cd3

• Improve type inference with a new rule allowing direct substitution

  ticki

  committed
  71f2d8b

  Copy full SHA for 71f2d8b

• Add section on impl unification

  ticki

  committed
  b355811

  Copy full SHA for b355811

• Add transitivity suggestion

  ticki

  committed
  a705532

  Copy full SHA for a705532

• Change syntax, add transitivity rule

  ticki

  committed
  946aa55

  Copy full SHA for 946aa55

• Add 'How we teach this'

  ticki

  committed
  d52e728

  Copy full SHA for d52e728

• Fix the code example

  ticki

  committed
  551688c

  Copy full SHA for 551688c

• Add optional extension

  ticki

  committed
  ea92a57

  Copy full SHA for ea92a57

• s/baz/foo

  ticki

  committed
  1d8813b

  Copy full SHA for 1d8813b

• Use unicode for the lines

  ticki

  committed
  d6a9b05

  Copy full SHA for d6a9b05

Commits on Jun 23, 2016

• Expand on the implication checking and the rules governing it

  ticki

  committed
  99b2005

  Copy full SHA for 99b2005

• Add subsection of 'motivation' dedicated to examples, at exit-point identities

  ticki

  committed
  60467c2

  Copy full SHA for 60467c2

• Expand motivation with aims

  ticki

  committed
  468f16a

  Copy full SHA for 468f16a

• Double negation and division by zero handling

  ticki

  committed
  a01250c

  Copy full SHA for a01250c

• Prove decidability

  ticki

  committed
  817ec48

  Copy full SHA for 817ec48

• Thanks for the feedback, gnzlbg, killercup, and kennytm

  ticki

  committed
  d46f550

  Copy full SHA for d46f550

• "Informalize" the rules

  ticki

  committed
  54e00af

  Copy full SHA for 54e00af

• Fix some typos in Pi Types RFCs

  Show description for 5718d4b
  killercup

  authored
  5718d4b

  Copy full SHA for 5718d4b

• Merge pull request #1 from killercup/patch-1

  Show description for 386de25
  ticki

  authored
  386de25

  Copy full SHA for 386de25

• Add section on SMT-solvers, fix gnzlbg's notes

  ticki

  committed
  dc4635a

  Copy full SHA for dc4635a

• Merge branch 'pi-types' of github.com:Ticki/rfcs into pi-types

  ticki

  committed
  d75674b

  Copy full SHA for d75674b

• Add remark

  ticki

  committed
  4e36bed

  Copy full SHA for 4e36bed

• Add section on possible extensions

  ticki

  committed
  b555120

  Copy full SHA for b555120

• Fix title on the second question

  ticki

  committed
  892e3d6

  Copy full SHA for 892e3d6

• Add section on structural equality, add symbolic implication

  ticki

  committed
  754b944

  Copy full SHA for 754b944

• Fix structural equality section

  ticki

  committed
  c7a2f28

  Copy full SHA for c7a2f28

• Add alternative with inherited bounds

  ticki

  committed
  9573c4d

  Copy full SHA for 9573c4d

Commits on Jun 24, 2016

• Move the SMT-section

  ticki

  committed
  74ef189

  Copy full SHA for 74ef189

• Add Hoare-based value/type optional extension

  ticki

  committed
  9f06922

  Copy full SHA for 9f06922

• Fix typos

  ticki

  committed
  6b88ae5

  Copy full SHA for 6b88ae5

• Transcription rules for inequalities

  ticki

  committed
  998c292

  Copy full SHA for 998c292

• Clarify notation

  ticki

  committed
  09aef59

  Copy full SHA for 09aef59

Commits on Jun 25, 2016

• Typos

  ticki

  committed
  0f3a499

  Copy full SHA for 0f3a499

Commits on Jun 27, 2016

• Fix typos

  ticki

  committed
  2dbfe2d

  Copy full SHA for 2dbfe2d