Skip to content

Commit 457f25f

Browse files
committed
Move typeOf function
1 parent 8f5a720 commit 457f25f

File tree

2 files changed

+6
-5
lines changed

2 files changed

+6
-5
lines changed

experiments/idris/src/Fathom/Base.idr

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,12 @@ import Data.List
77
import Data.Vect
88

99

10+
||| Return the type of an expression, without consuming it
11+
public export
12+
typeOf : {1 A : Type} -> (0 x : A) -> Type
13+
typeOf _ = A
14+
15+
1016
---------------------------
1117
-- ENCODER/DECODER PAIRS --
1218
---------------------------

experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,6 @@ import Fathom.Data.Iso
1414
import Fathom.Data.Sing
1515

1616

17-
public export
18-
typeOf : {1 A : Type} -> (0 x : A) -> Type
19-
typeOf _ = A
20-
21-
2217
-------------------------
2318
-- FORMAT DESCRIPTIONS --
2419
-------------------------

0 commit comments

Comments
 (0)