Skip to content

Commit 61f7cc5

Browse files
author
Matthew Mirman
committed
uncommented out logic
1 parent 012694d commit 61f7cc5

File tree

1 file changed

+2
-4
lines changed

1 file changed

+2
-4
lines changed

prelude/logic.ncc

+2-4
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
{-
21
-------------
32
-- exists --
43
-------------
@@ -29,12 +28,12 @@ defn open : {N}{F : N -> type}{A : type} ( exists a : N . F a ) -> ([a : N] F a
2928
-- searches ---
3029
---------------
3130

32-
-}
31+
3332

3433
defn any : {Search : type} (Search -> type) -> type
3534
| is = [V : A][F : A -> type] F V -> any {Search = A} F
3635

37-
{-
36+
3837

3938

4039
defn openAny : [A][F : A -> type] any F -> [V : A] F V -> type
@@ -66,4 +65,3 @@ fixity left 0 ==
6665
defn == : {q : type} (q -> type) -> q -> type
6766
as ?\q . \foo : q -> type . \v : q . foo v
6867

69-
-}

0 commit comments

Comments
 (0)