@@ -17,7 +17,7 @@ Exporting Idris Functions
17
17
"returnType": "String"
18
18
}
19
19
"""
20
- exportStringReplicate :Nat -> Char -> String
20
+ exportStringReplicate : Nat -> Char -> String
21
21
exportStringReplicate = String.replicate
22
22
23
23
This code exports ``replicate `` function from ``Data.String `` Idris module. The export block starting with ``%export ``
@@ -87,7 +87,7 @@ integers which Java code shouldn't rely on.
87
87
idris/data/List
88
88
helloworld/Color
89
89
"""
90
- typeExports: List String
90
+ typeExports : List String
91
91
typeExports = []
92
92
93
93
Similar to ``jvmExports `` block explained above, ``typeExports `` is a special export function that exports Idris types
@@ -112,7 +112,7 @@ Exporting Idris functions with Generic Types
112
112
jvm:export
113
113
IdrisList
114
114
"""
115
- typeExports: List String
115
+ typeExports : List String
116
116
typeExports = []
117
117
118
118
%export """
@@ -239,7 +239,7 @@ Here is a complete example in Idris and Java:
239
239
Show
240
240
Color
241
241
"""
242
- typeExports: List String
242
+ typeExports : List String
243
243
typeExports = []
244
244
245
245
%export """
@@ -462,6 +462,20 @@ Java calling the Idris functions:
462
462
463
463
}
464
464
465
+ This is the output:
466
+
467
+ .. code-block :: text
468
+
469
+ [23, 45]
470
+ ["foo", "bar"]
471
+ [Red, Blue]
472
+ Green
473
+ Blue
474
+ Just Green
475
+ Nothing
476
+ AAAAAAAAAA
477
+
478
+
465
479
Here line numbers 29-33 retrieve type class instances for different types and the instances are passed in the lines
466
480
below when ``show `` function is called. Another thing to note here is that when we call generic Idris functions, Idris
467
481
types that are wrapped in Java types needs to be converted before passing to Idris functions. For example, line 23
0 commit comments