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
Age
Commit message (
Expand
)
Author
2023-04-23
Rename for clarity.
Chloe Brown
2023-04-23
Prove reducibility is reflexive.
Chloe Brown
2023-04-23
Use custom relation for even more control.
Chloe Brown
2023-04-22
Package a visible induction statement.
Chloe Brown
2023-04-22
Define logical relation.
Chloe Brown
2023-04-16
Define generic equality.
Chloe Brown
2023-04-16
Prove weakening of reduction.
Chloe Brown
2023-04-16
Prove weakening of type judgements.
Chloe Brown
2023-04-16
Define environment extensions.
Chloe Brown
2023-04-16
Prove weakening a thinned term is homomorphic.
Chloe Brown
2023-04-16
Prove more properties about thinning composition.
Chloe Brown
2023-04-16
Prove reduction is deterministic.
Chloe Brown
2023-04-16
Prove whnfs do not reduce.
Chloe Brown
2023-04-16
Prove subject typing.
Chloe Brown
2023-04-16
Prove conversion subsumes reduction.
Chloe Brown
2023-04-16
Define term reduction.
Chloe Brown
2023-04-15
Prove environments are well-formed.
Chloe Brown
2023-04-15
Prove typing respects environment quotient.
Chloe Brown
2023-04-15
Define declarative typing rules.
Chloe Brown
2023-04-15
Define typing environments.
Chloe Brown
2023-04-15
Prove substitution respects the quotient.
Chloe Brown
2023-04-15
Define Term substitution.
Chloe Brown
2023-04-14
Define weakening.
Chloe Brown
2023-04-14
Define Thinnings.
Chloe Brown
2023-04-14
Define Terms.
Chloe Brown