Skip to content

Commit 0423601

Browse files
committed
test: also test fn
1 parent 9f8fabb commit 0423601

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

Diff for: cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java

+5
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,11 @@ public class ReplCompilerTest {
5454
| suc (_ : Nat)
5555
""".trim(), Nat.core().easyToString());
5656

57+
var refl = assertInstanceOf(CompiledVar.class, findContext("Path::refl"));
58+
assertNotNull(refl);
59+
assertEquals("def refl {A : Type 0} {a : A} : a = a => /* compiled code */",
60+
refl.core().easyToString());
61+
5762
// Don't be too harsh on the test lib structure, maybe we will change it
5863
var rootHints = compiler.getContext().giveMeHint(ImmutableSeq.empty());
5964
assertTrue(rootHints.contains("Nat"));

0 commit comments

Comments
 (0)