Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RFC: const-dependent type system. #1657

Closed
wants to merge 36 commits into from
Closed

RFC: const-dependent type system. #1657

Changes from all commits
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
27c33a3
rfc: Π-types
ticki Jun 22, 2016
e4446c5
Expand the `overview` section
ticki Jun 22, 2016
eb60cd3
Propose alternative syntaxes
ticki Jun 22, 2016
71f2d8b
Improve type inference with a new rule allowing direct substitution
ticki Jun 22, 2016
b355811
Add section on impl unification
ticki Jun 22, 2016
a705532
Add transitivity suggestion
ticki Jun 22, 2016
946aa55
Change syntax, add transitivity rule
ticki Jun 22, 2016
d52e728
Add 'How we teach this'
ticki Jun 22, 2016
551688c
Fix the code example
ticki Jun 22, 2016
ea92a57
Add optional extension
ticki Jun 22, 2016
1d8813b
s/baz/foo
ticki Jun 22, 2016
d6a9b05
Use unicode for the lines
ticki Jun 22, 2016
99b2005
Expand on the implication checking and the rules governing it
ticki Jun 23, 2016
60467c2
Add subsection of 'motivation' dedicated to examples, at exit-point i…
ticki Jun 23, 2016
468f16a
Expand motivation with aims
ticki Jun 23, 2016
a01250c
Double negation and division by zero handling
ticki Jun 23, 2016
817ec48
Prove decidability
ticki Jun 23, 2016
d46f550
Thanks for the feedback, gnzlbg, killercup, and kennytm
ticki Jun 23, 2016
54e00af
"Informalize" the rules
ticki Jun 23, 2016
5718d4b
Fix some typos in Pi Types RFCs
killercup Jun 23, 2016
386de25
Merge pull request #1 from killercup/patch-1
ticki Jun 23, 2016
dc4635a
Add section on SMT-solvers, fix gnzlbg's notes
ticki Jun 23, 2016
d75674b
Merge branch 'pi-types' of github.com:Ticki/rfcs into pi-types
ticki Jun 23, 2016
4e36bed
Add remark
ticki Jun 23, 2016
b555120
Add section on possible extensions
ticki Jun 23, 2016
892e3d6
Fix title on the second question
ticki Jun 23, 2016
754b944
Add section on structural equality, add symbolic implication
ticki Jun 23, 2016
c7a2f28
Fix structural equality section
ticki Jun 23, 2016
9573c4d
Add alternative with inherited bounds
ticki Jun 23, 2016
74ef189
Move the SMT-section
ticki Jun 24, 2016
9f06922
Add Hoare-based value/type optional extension
ticki Jun 24, 2016
6b88ae5
Fix typos
ticki Jun 24, 2016
998c292
Transcription rules for inequalities
ticki Jun 24, 2016
09aef59
Clarify notation
ticki Jun 24, 2016
0f3a499
Typos
ticki Jun 25, 2016
2dbfe2d
Fix typos
ticki Jun 27, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading