mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-23 09:52:55 -06:00
*** empty log message ***
This commit is contained in:
@@ -27,7 +27,7 @@ fun
|
|||||||
|
|
||||||
Univ : (A : Dom) -> (Elem A -> Prop) -> Prop ;
|
Univ : (A : Dom) -> (Elem A -> Prop) -> Prop ;
|
||||||
Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
|
Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
|
||||||
|
|
||||||
-- progressive implication ŕ la type theory
|
-- progressive implication ŕ la type theory
|
||||||
ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
|
ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user