diff options
| author | peb <unknown> | 2004-08-10 09:40:35 +0000 |
|---|---|---|
| committer | peb <unknown> | 2004-08-10 09:40:35 +0000 |
| commit | d045a9884858f7cf73b5914f68a93b6e405a1682 (patch) | |
| tree | 3c2b6fa276124c28cdbd9cbd8d5c310a4504792e | |
| parent | 9650864b06bbc90c5e2f64c36cf0c67c68300af5 (diff) | |
*** empty log message ***
| -rw-r--r-- | grammars/logic/Logic.gf | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf index 334592946..3e2516ebc 100644 --- a/grammars/logic/Logic.gf +++ b/grammars/logic/Logic.gf @@ -27,7 +27,7 @@ fun Univ : (A : Dom) -> (Elem A -> Prop) -> Prop ; Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ; - + -- progressive implication à la type theory ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ; |