index
:
yellowsquid/correct-obs.git
master
nameless
[no description]
Chloe Brown
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Core
/
Declarative.idr
Age
Commit message (
Collapse
)
Author
2023-04-08
Prove conversion is a generic equality.
HEAD
master
Chloe Brown
2023-04-08
Prove weakening preserves reduction.
Chloe Brown
2023-04-08
Reduce code duplication.
Chloe Brown
2023-04-07
Prove weakening preserves typing judgements.
Chloe Brown
2023-04-07
Correct definition of Eta conversion.
Chloe Brown
2023-04-06
Move and rename ThinWf.
Chloe Brown
Correct statement for weakening preservation.
2023-04-06
Migrate Env to use Thinned.
Chloe Brown
2023-04-02
Move Environment module.
Chloe Brown
2023-04-02
State that weakening preserves typing.
Chloe Brown
2023-04-02
Prove environment equality preserves typing.
Chloe Brown
2023-04-01
State typing respects environment equality.
Chloe Brown
2023-04-01
Prove composition of thinnings is well-formed.
Chloe Brown
2023-04-01
Define well-formed thinnings.
Chloe Brown
2023-04-01
Make environments do weakening lazily.
Chloe Brown
This is in anticipation for defining well-formed thinnings.
2023-04-01
Prove typing implies a well-formed environment.
Chloe Brown
2023-04-01
State properties of typing and reduction.
Chloe Brown
There correspond to lemmata 2.1--2.5 in Abel et. al.
2023-04-01
Define Declarative typing rules.
Chloe Brown
