diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 13:19:46 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 13:30:47 +0100 |
| commit | 0cce62f5e290d059b1545006c11b33d4329f00a3 (patch) | |
| tree | 48d76e2f8ad1cbb233b8fdb12832be597a800cd1 /src/Core/Declarative.idr | |
| parent | c62b9753293389c37f29089a856a5d9a42ea23d5 (diff) | |
State properties of typing and reduction.
There correspond to lemmata 2.1--2.5 in Abel et. al.
Diffstat (limited to 'src/Core/Declarative.idr')
| -rw-r--r-- | src/Core/Declarative.idr | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 2561797..99cc1ab 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -146,3 +146,10 @@ data TermConv where %name TypeConv conv %name TermWf wf %name TermConv conv + +-- Well Formed Environment ----------------------------------------------------- + +typeWfImpliesEnvWf : TypeWf env a -> EnvWf env +typeConvImpliesEnvWf : TypeConv env a b -> EnvWf env +termWfImpliesEnvWf : TermWf env t a -> EnvWf env +termConvImpliesEnvWf : TermConv env t u a -> EnvWf env |