From 1b4abb8fdd81f6de2166ef3f064a77fd5622fe83 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 6 May 2026 11:21:22 +0100 Subject: clean up examples vs tests --- examples/tests/test_alpha_equiv.makkai | 4 ++++ examples/tests/test_ext_codomain.makkai | 5 +++++ examples/tests/test_inline_nested.makkai | 9 +++++++++ examples/tests/test_nested_for.makkai | 3 +++ examples/tests/test_signature_merge.makkai | 12 ++++++++++++ examples/tests/test_signature_param.makkai | 4 ++++ 6 files changed, 37 insertions(+) create mode 100644 examples/tests/test_alpha_equiv.makkai create mode 100644 examples/tests/test_ext_codomain.makkai create mode 100644 examples/tests/test_inline_nested.makkai create mode 100644 examples/tests/test_nested_for.makkai create mode 100644 examples/tests/test_signature_merge.makkai create mode 100644 examples/tests/test_signature_param.makkai (limited to 'examples/tests') diff --git a/examples/tests/test_alpha_equiv.makkai b/examples/tests/test_alpha_equiv.makkai new file mode 100644 index 0000000..2ae067a --- /dev/null +++ b/examples/tests/test_alpha_equiv.makkai @@ -0,0 +1,4 @@ +let signature S = (n : Nat) -> Set +let signature T = (m : Nat) -> Set +let instance i :: S = for (x : Nat), (Nat :: Set) +let instance j :: T = i diff --git a/examples/tests/test_ext_codomain.makkai b/examples/tests/test_ext_codomain.makkai new file mode 100644 index 0000000..da0ddae --- /dev/null +++ b/examples/tests/test_ext_codomain.makkai @@ -0,0 +1,5 @@ +let signature S = (x : Nat) -> theory { G :: Set } + +let instance s :: S = for (x : Nat), { .G = (Nat :: Set) } + +let set NatAgain = set-of((s 42) .G) diff --git a/examples/tests/test_inline_nested.makkai b/examples/tests/test_inline_nested.makkai new file mode 100644 index 0000000..e891349 --- /dev/null +++ b/examples/tests/test_inline_nested.makkai @@ -0,0 +1,9 @@ +let signature Outer = theory { + Inner :: theory { F :: Set } +} + +let instance my_outer :: Outer = { + .Inner = { .F = (Nat :: Set) } +} + +let set MyF = set-of(my_outer .Inner .F) diff --git a/examples/tests/test_nested_for.makkai b/examples/tests/test_nested_for.makkai new file mode 100644 index 0000000..b3618cc --- /dev/null +++ b/examples/tests/test_nested_for.makkai @@ -0,0 +1,3 @@ +let signature F = (n : Nat) -> (m : Nat) -> Set +let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set) +let set Result = set-of(f 1 2) diff --git a/examples/tests/test_signature_merge.makkai b/examples/tests/test_signature_merge.makkai new file mode 100644 index 0000000..5f575d5 --- /dev/null +++ b/examples/tests/test_signature_merge.makkai @@ -0,0 +1,12 @@ +let signature S = (n : Nat) -> Set +let signature U = (k : Bool) -> S +let signature W = (k : Bool)(n : Nat) -> Set + +let instance u :: U = for (k : Bool), for (n : Nat), (Nat :: Set) +let instance w :: W = u + +let signature F = (n : Nat) (m : Nat) -> Set +let signature G = (n : Nat) -> (m : Nat) -> Set + +let instance f :: F = for (n : Nat) (m : Nat), (Nat :: Set) +let instance g :: G = f diff --git a/examples/tests/test_signature_param.makkai b/examples/tests/test_signature_param.makkai new file mode 100644 index 0000000..9dae31b --- /dev/null +++ b/examples/tests/test_signature_param.makkai @@ -0,0 +1,4 @@ +let signature S = theory { + F :: (x : Nat) (y : Bool) -> Set, + G :: (z : set-of(F 3 4)) -> Set // this sould fail +} -- cgit v1.3.1