search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.35k stars 304 forks source link

Turn Γ into a parameter. #545

Open xekoukou opened 3 years ago

xekoukou commented 3 years ago

https://github.com/plfa/plfa.github.io/blame/dev/src/plfa/part2/DeBruijn.lagda.md#L783

In the Value definition, the context can be a parameter.

wenkokke commented 3 years ago

If you're happy to submit a pull-request updating the definitions of Value in DeBruijn and More, I'd be happy to merge it!