This website requires JavaScript.
Explore
Help
Sign In
minze
/
univTypes
Watch
1
Star
0
Fork
0
You've already forked univTypes
Code
Issues
Pull Requests
Actions
Packages
Projects
Releases
Wiki
Activity
Files
main
univTypes
/
SubjectReduction
T
Add File
New File
Upload File
Apply Patch
Copy Permalink
Download directory as ZIP
Download directory as TAR.GZ
Delete Directory
History
JKF
201fe7942b
Make β-λ more generic (Argument can now be any type T instead of `Setn L)
2026-04-25 22:24:28 +02:00
..
Composition.agda
changes
2026-04-17 19:31:44 +02:00
Confluence.agda
small work
2026-04-21 20:44:15 +02:00
ConversionProperties.agda
Some definitions and adjusted proofs
2026-04-25 21:57:10 +02:00
Inversion.agda
Make β-λ more generic (Argument can now be any type T instead of `Setn L)
2026-04-25 22:24:28 +02:00
Specification.agda
Make β-λ more generic (Argument can now be any type T instead of `Setn L)
2026-04-25 22:24:28 +02:00
SubjectReduction.agda
Some definitions and adjusted proofs
2026-04-25 21:57:10 +02:00
SubstitutionPreservesTyping.agda
Some definitions and adjusted proofs
2026-04-25 21:57:10 +02:00
JKF