diff options
| -rw-r--r-- | src/Core/Declarative.idr | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 99cc1ab..8efda89 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -153,3 +153,28 @@ 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 + +typeWfImpliesEnvWf (SetType envWf) = envWf +typeWfImpliesEnvWf (PiType wf wf1) = typeWfImpliesEnvWf wf +typeWfImpliesEnvWf (LiftType wf) = termWfImpliesEnvWf wf + +typeConvImpliesEnvWf (ReflType wf) = typeWfImpliesEnvWf wf +typeConvImpliesEnvWf (SymType conv) = typeConvImpliesEnvWf conv +typeConvImpliesEnvWf (TransType conv conv1) = typeConvImpliesEnvWf conv +typeConvImpliesEnvWf (PiTypeConv wf conv conv1) = typeConvImpliesEnvWf conv +typeConvImpliesEnvWf (LiftConv conv) = termConvImpliesEnvWf conv + +termWfImpliesEnvWf (VarTerm envWf) = envWf +termWfImpliesEnvWf (PiTerm wf wf1) = termWfImpliesEnvWf wf +termWfImpliesEnvWf (AbsTerm wf wf1) = typeWfImpliesEnvWf wf +termWfImpliesEnvWf (AppTerm wf wf1) = termWfImpliesEnvWf wf +termWfImpliesEnvWf (ConvTerm wf conv) = termWfImpliesEnvWf wf + +termConvImpliesEnvWf (ReflTerm wf) = termWfImpliesEnvWf wf +termConvImpliesEnvWf (SymTerm conv) = termConvImpliesEnvWf conv +termConvImpliesEnvWf (TransTerm conv conv1) = termConvImpliesEnvWf conv +termConvImpliesEnvWf (ConvTermConv conv conv1) = termConvImpliesEnvWf conv +termConvImpliesEnvWf (PiTermConv wf conv conv1) = termConvImpliesEnvWf conv +termConvImpliesEnvWf (PiBeta wf wf1 wf2) = typeWfImpliesEnvWf wf +termConvImpliesEnvWf (PiEta wf wf1 wf2 conv) = typeWfImpliesEnvWf wf +termConvImpliesEnvWf (AppConv conv conv1) = termConvImpliesEnvWf conv |