diff options
| author | aarne <unknown> | 2005-09-13 21:05:32 +0000 |
|---|---|---|
| committer | aarne <unknown> | 2005-09-13 21:05:32 +0000 |
| commit | 95463f6dbae318b055e2cb7927ac7acb320c8382 (patch) | |
| tree | 994469bca26a90fff98c94220e60daf990acb74d /grammars | |
| parent | 314a9db89f93ca6895595268485fe23a6c85c07a (diff) | |
fix in tc
Diffstat (limited to 'grammars')
| -rw-r--r-- | grammars/logic/Logic.gf | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf index 41fd5cef8..5f49fc2e1 100644 --- a/grammars/logic/Logic.gf +++ b/grammars/logic/Logic.gf @@ -73,7 +73,8 @@ fun Pron : (A : Dom) -> Elem A -> Elem A ; def - -- proof normalization + -- proof normalization; does not tc 13/9/2005 + ConjEl _ _ (ConjI _ _ a _) = a ; ConjEr _ _ (ConjI _ _ _ b) = b ; DisjE _ _ _ (DisjIl _ _ a) d _ = d a ; @@ -81,7 +82,11 @@ def ImplE _ _ (ImplI _ _ b) a = b a ; NegE _ (NegI _ b) a = b a ; UnivE _ _ (UnivI _ _ b) a = b a ; - ExistE _ _ _ (ExistI _ _ a b) d = d a b ; +--- ExistE _ _ _ (ExistI _ _ a b) d = d a b ; +--- does not tc 13/9/2005: {a{-2-}<>a{-0-}} +--- moreover: no problem with +--- ConjEr _ _ (ConjI _ _ a _) = a ; +--- But this changes when A B are used instead of _ _ -- Hypo and Pron are identities Hypo _ a = a ; |