diff --git a/.github/workflows/ci-edric-types.yml b/.github/workflows/ci-edric-types.yml index b118d49446..85b82f4d5e 100644 --- a/.github/workflows/ci-edric-types.yml +++ b/.github/workflows/ci-edric-types.yml @@ -4,18 +4,22 @@ on: pull_request: paths: - 'examples/units-time-intervals/**' + - 'examples/linear-geometry-type-core/**' - 'tests/idris2/basic/edric007/**' + - 'tests/idris2/basic/edric008/**' - 'edric' - '.github/workflows/ci-edric-types.yml' push: paths: - 'examples/units-time-intervals/**' + - 'examples/linear-geometry-type-core/**' - 'tests/idris2/basic/edric007/**' + - 'tests/idris2/basic/edric008/**' - 'edric' - '.github/workflows/ci-edric-types.yml' jobs: - units-time-intervals: + settled-type-cores: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 diff --git a/edric b/edric index 2bcee11b8d..bf806d3588 100755 --- a/edric +++ b/edric @@ -42,6 +42,7 @@ smoke_test() { "$make_command" -C "$repo_root" test only=idris2/basic/edric005 "$make_command" -C "$repo_root" test only=idris2/basic/edric006 "$make_command" -C "$repo_root" test only=idris2/basic/edric007 + "$make_command" -C "$repo_root" test only=idris2/basic/edric008 } command=${1:-all} @@ -67,4 +68,4 @@ all) usage >&2 exit 2 ;; -esac +esac \ No newline at end of file diff --git a/examples/linear-geometry-type-core/LinearGeometryTypes.idric b/examples/linear-geometry-type-core/LinearGeometryTypes.idric new file mode 100644 index 0000000000..2040eb5a26 --- /dev/null +++ b/examples/linear-geometry-type-core/LinearGeometryTypes.idric @@ -0,0 +1,357 @@ +module LinearGeometryTypes + +%default total + +-- This is an executable type-system slice for settled linear/elementary +-- geometry. It is deliberately not a complete real-number implementation. +-- ExactRealVector uses Integer coordinates as exact sample points embedded in +-- R^n so the compiler can execute the structural tests without introducing a +-- floating-point policy here. The dimension/orientation/topology interfaces +-- are the part under test; a later scalar layer can widen the coordinates. + +-- -------------------------------------------------------------------------- +-- 1. Dimension-indexed mathematical vectors +-- -------------------------------------------------------------------------- + +public export +data ExactRealVector : Nat -> Type where + VNil : ExactRealVector Z + VCons : Integer -> ExactRealVector n -> ExactRealVector (S n) + +public export +add : ExactRealVector n -> ExactRealVector n -> ExactRealVector n +add VNil VNil = VNil +add (VCons x xs) (VCons y ys) = VCons (x + y) (add xs ys) + +public export +negateVector : ExactRealVector n -> ExactRealVector n +negateVector VNil = VNil +negateVector (VCons x xs) = VCons (-x) (negateVector xs) + +public export +difference : ExactRealVector n -> ExactRealVector n -> ExactRealVector n +difference VNil VNil = VNil +difference (VCons x xs) (VCons y ys) = VCons (x - y) (difference xs ys) + +public export +dot : ExactRealVector n -> ExactRealVector n -> Integer +dot VNil VNil = 0 +dot (VCons x xs) (VCons y ys) = x * y + dot xs ys + +public export +squaredNorm : ExactRealVector n -> Integer +squaredNorm x = dot x x + +public export +squaredDistance : ExactRealVector n -> ExactRealVector n -> Integer +squaredDistance x y = squaredNorm (difference x y) + +-- Approximation thresholds remain explicit. The type system may require that +-- both operands inhabit the same ambient dimension; it must not invent the +-- application-specific epsilon that says two semantic displacements are close. +public export +withinSquaredTolerance : + Integer -> ExactRealVector n -> ExactRealVector n -> Bool +withinSquaredTolerance tolerance x y = squaredDistance x y <= tolerance + +public export +data SemanticEmbedding : Nat -> Type where + Embedding : ExactRealVector n -> SemanticEmbedding n + +public export +semanticResidual : + SemanticEmbedding n -> SemanticEmbedding n -> ExactRealVector n +semanticResidual (Embedding x) (Embedding y) = difference x y + +public export +semanticWithinSquaredTolerance : + Integer -> SemanticEmbedding n -> SemanticEmbedding n -> Bool +semanticWithinSquaredTolerance tolerance (Embedding x) (Embedding y) = + withinSquaredTolerance tolerance x y + +-- -------------------------------------------------------------------------- +-- 2. Quaternion sample algebra +-- -------------------------------------------------------------------------- + +-- Integer coefficients give an executable exact subring of the quaternion +-- algebra. The multiplication laws are the ordinary Hamilton laws; this does +-- not claim that the eventual scalar type for H should be Integer. +public export +data Quaternion = Q Integer Integer Integer Integer + +public export +quaternionNegate : Quaternion -> Quaternion +quaternionNegate (Q a b c d) = Q (-a) (-b) (-c) (-d) + +public export +quaternionMultiply : Quaternion -> Quaternion -> Quaternion +quaternionMultiply (Q a b c d) (Q e f g h) = + Q + (a * e - b * f - c * g - d * h) + (a * f + b * e + c * h - d * g) + (a * g - b * h + c * e + d * f) + (a * h + b * g - c * f + d * e) + +public export +quaternionNormSquared : Quaternion -> Integer +quaternionNormSquared (Q a b c d) = + a * a + b * b + c * c + d * d + +public export +quatOne : Quaternion +quatOne = Q 1 0 0 0 + +public export +quatI : Quaternion +quatI = Q 0 1 0 0 + +public export +quatJ : Quaternion +quatJ = Q 0 0 1 0 + +public export +quatK : Quaternion +quatK = Q 0 0 0 1 + +-- A unit sample carries the norm-one certificate. This is intentionally a +-- dependent value, not a Boolean tag that can drift away from its quaternion. +public export +data UnitQuaternion : Type where + UnitQuaternionValue : + (q : Quaternion) -> quaternionNormSquared q = 1 -> UnitQuaternion + +public export +unitQuatOne : UnitQuaternion +unitQuatOne = UnitQuaternionValue quatOne Refl + +public export +unitQuatI : UnitQuaternion +unitQuatI = UnitQuaternionValue quatI Refl + +public export +unitQuatJ : UnitQuaternion +unitQuatJ = UnitQuaternionValue quatJ Refl + +public export +unitQuatK : UnitQuaternion +unitQuatK = UnitQuaternionValue quatK Refl + +-- -------------------------------------------------------------------------- +-- 3. O(n), SO(n), reflections, and exact rotation generators +-- -------------------------------------------------------------------------- + +public export +data Orientation = Preserving | Reversing + +public export +composeOrientation : Orientation -> Orientation -> Orientation +composeOrientation Preserving Preserving = Preserving +composeOrientation Preserving Reversing = Reversing +composeOrientation Reversing Preserving = Reversing +composeOrientation Reversing Reversing = Preserving + +-- There is deliberately no "arbitrary matrix is orthogonal" constructor. +-- Every constructor below denotes a transformation whose orthogonality is +-- settled mathematically, and composition preserves that invariant. +-- +-- FirstPlaneQuarterTurnTransform is the exact Givens rotation in the first +-- coordinate plane with c = 0, s = 1. It works in any ambient dimension >= 2. +-- General-angle/arbitrary-axis Givens rotations can be added when the scalar +-- and trigonometric representation is settled. +public export +data OrthogonalTransform : Nat -> Orientation -> Type where + OrthogonalIdentity : OrthogonalTransform n Preserving + FirstAxisReflection : OrthogonalTransform (S n) Reversing + FirstPlaneQuarterTurnTransform : + OrthogonalTransform (S (S n)) Preserving + QuaternionRotationTransform : + UnitQuaternion -> OrthogonalTransform 3 Preserving + ComposeOrthogonal : + OrthogonalTransform n left -> + OrthogonalTransform n right -> + OrthogonalTransform n (composeOrientation left right) + +public export +data SpecialOrthogonal : Nat -> Type where + InSO : OrthogonalTransform n Preserving -> SpecialOrthogonal n + +public export +firstAxisReflection : OrthogonalTransform (S n) Reversing +firstAxisReflection = FirstAxisReflection + +public export +firstPlaneQuarterTurn : SpecialOrthogonal (S (S n)) +firstPlaneQuarterTurn = InSO FirstPlaneQuarterTurnTransform + +public export +composeOrthogonal : + OrthogonalTransform n left -> + OrthogonalTransform n right -> + OrthogonalTransform n (composeOrientation left right) +composeOrthogonal = ComposeOrthogonal + +public export +twoReflections : + OrthogonalTransform n Reversing -> + OrthogonalTransform n Reversing -> + SpecialOrthogonal n +twoReflections left right = InSO (ComposeOrthogonal left right) + +public export +quaternionRotation : UnitQuaternion -> SpecialOrthogonal 3 +quaternionRotation q = InSO (QuaternionRotationTransform q) + +public export +soTransform : SpecialOrthogonal n -> OrthogonalTransform n Preserving +soTransform (InSO transform) = transform + +-- -------------------------------------------------------------------------- +-- 4. Spheres and orthogonal actions +-- -------------------------------------------------------------------------- + +-- UnitSpherePoint n means a point of S^n in ambient R^(n+1). A checked exact +-- coordinate sample carries its norm-one equality. OrthogonalImage records the +-- standard theorem that O(n+1) preserves the unit sphere without asking the +-- elaborator to rediscover that theorem from coordinate arithmetic each time. +public export +data UnitSpherePoint : Nat -> Type where + CheckedUnitSpherePoint : + (coordinates : ExactRealVector (S n)) -> + squaredNorm coordinates = 1 -> + UnitSpherePoint n + OrthogonalImage : + OrthogonalTransform (S n) orientation -> + UnitSpherePoint n -> + UnitSpherePoint n + +public export +actOnUnitSphere : + OrthogonalTransform (S n) orientation -> UnitSpherePoint n -> UnitSpherePoint n +actOnUnitSphere transform point = OrthogonalImage transform point + +public export +actSOOnUnitSphere : + SpecialOrthogonal (S n) -> UnitSpherePoint n -> UnitSpherePoint n +actSOOnUnitSphere rotation point = OrthogonalImage (soTransform rotation) point + +public export +northPoleS2 : UnitSpherePoint 2 +northPoleS2 = + CheckedUnitSpherePoint + (VCons 0 (VCons 0 (VCons 1 VNil))) + Refl + +-- Integral cohomology ranks of ordinary spheres. The S^0 case is explicit: +-- it has two connected components, so H^0(S^0; Z) has rank 2. For n > 0 the +-- only nonzero ranks are degree 0 and degree n, both rank 1. Odd/even spheres +-- therefore do NOT differ at this additive-rank level. +public export +sphereIntegralCohomologyRank : Nat -> Nat -> Nat +sphereIntegralCohomologyRank Z Z = 2 +sphereIntegralCohomologyRank Z (S degree) = 0 +sphereIntegralCohomologyRank (S dimension) Z = 1 +sphereIntegralCohomologyRank (S dimension) (S degree) = + if dimension == degree then 1 else 0 + +public export +data Parity = Even | Odd + +public export +flipParity : Parity -> Parity +flipParity Even = Odd +flipParity Odd = Even + +public export +natParity : Nat -> Parity +natParity Z = Even +natParity (S n) = flipParity (natParity n) + +-- chi(S^n) = 1 + (-1)^n. +public export +sphereEulerCharacteristic : Nat -> Integer +sphereEulerCharacteristic dimension = + case natParity dimension of + Even => 2 + Odd => 0 + +-- -------------------------------------------------------------------------- +-- 5. Complex projective-space facts used as typed library knowledge +-- -------------------------------------------------------------------------- + +-- CP^n has complex dimension n and real dimension 2n. +public export +cpRealDimension : Nat -> Nat +cpRealDimension n = n + n + +-- The Hopf quotient presentation is CP^n = S^(2n+1) / S^1. This function +-- returns the dimension of the sphere appearing in that standard presentation. +public export +cpHopfSphereDimension : Nat -> Nat +cpHopfSphereDimension n = S (n + n) + +-- Additive integral cohomology ranks of CP^n: rank 1 in even degrees +-- 0,2,...,2n and 0 otherwise. Ring structure Z[x]/(x^(n+1)), |x|=2, is a +-- separate theorem-level fact and is deliberately not faked as a polynomial +-- implementation in this small slice. +public export +cpIntegralCohomologyRank : Nat -> Nat -> Nat +cpIntegralCohomologyRank n Z = 1 +cpIntegralCohomologyRank Z (S degree) = 0 +cpIntegralCohomologyRank (S n) (S Z) = 0 +cpIntegralCohomologyRank (S n) (S (S degree)) = + cpIntegralCohomologyRank n degree + +public export +data HopfQuotientFact : Nat -> Type where + CPnAsSphereByCircle : (n : Nat) -> HopfQuotientFact n + +public export +cpHopfQuotient : (n : Nat) -> HopfQuotientFact n +cpHopfQuotient n = CPnAsSphereByCircle n + +-- -------------------------------------------------------------------------- +-- 6. Named standard topology facts +-- -------------------------------------------------------------------------- + +-- These values represent theorem-library entries, not compiler-generated +-- proofs. The intended future elaborator boundary from #42 is: if hypotheses +-- match a named checked theorem, the theorem may contribute a typed fact and an +-- explanation trace saying exactly which theorem was used. + +-- EmbeddedCircleInS2 stands for a genuine embedding S^1 -> S^2. The Jordan +-- curve theorem then gives exactly two connected components in the complement. +public export +data EmbeddedCircleInS2 = MkJordanCurveExample + +public export +jordanCurveExample : EmbeddedCircleInS2 +jordanCurveExample = MkJordanCurveExample + +public export +data JordanSeparation : EmbeddedCircleInS2 -> Type where + ExactlyTwoComplementComponents : + (curve : EmbeddedCircleInS2) -> JordanSeparation curve + +public export +jordanSeparation : (curve : EmbeddedCircleInS2) -> JordanSeparation curve +jordanSeparation curve = ExactlyTwoComplementComponents curve + +public export +complementComponentCount : JordanSeparation curve -> Nat +complementComponentCount (ExactlyTwoComplementComponents curve) = 2 + +-- For Euclidean R^n, the one-point compactification is S^n. This is a named +-- standard fact with the relevant family indexed explicitly; it is not a +-- generic magical compactify operation for arbitrary spaces. +public export +data EuclideanCompactificationFact : Nat -> Type where + EuclideanPlusIsSphere : (n : Nat) -> EuclideanCompactificationFact n + +public export +euclideanOnePointCompactification : + (n : Nat) -> EuclideanCompactificationFact n +euclideanOnePointCompactification n = EuclideanPlusIsSphere n + +public export +compactifiedSphereDimension : EuclideanCompactificationFact n -> Nat +compactifiedSphereDimension (EuclideanPlusIsSphere n) = n diff --git a/examples/linear-geometry-type-core/README.md b/examples/linear-geometry-type-core/README.md new file mode 100644 index 0000000000..c54855a53b --- /dev/null +++ b/examples/linear-geometry-type-core/README.md @@ -0,0 +1,38 @@ +# Linear geometry type core + +This is the bounded second pass after the exact units/time/interval slice. It is intentionally centered on finite-dimensional linear algebra rather than a broad inheritance hierarchy. + +## SETTLED and encoded here + +- dimension-indexed mathematical vectors: incompatible dimensions cannot be passed to subtraction, dot product, distance, or semantic-residual operations; +- explicit approximation thresholds: the compiler checks ambient compatibility but does not invent an application-specific semantic epsilon; +- orientation as a type index for orthogonal transformations; +- composition rules for orientation, including reflection × reflection landing in `SO(n)`; +- an exact first-axis reflection and a first-coordinate-plane quarter turn (a Givens rotation with `c = 0`, `s = 1`); +- `S^n` represented with ambient dimension `n + 1`, plus the standard `O(n+1)` action preserving sphere membership; +- integral cohomology ranks of spheres, with the `S^0` case handled separately; +- `chi(S^n) = 1 + (-1)^n`, so odd spheres have Euler characteristic 0 and even spheres 2; +- Hamilton quaternion multiplication on exact integer-coordinate samples, norm-one certificates, and the typed unit-quaternion-to-`SO(3)` boundary; +- `CP^n` real dimension `2n`, the Hopf presentation `S^(2n+1) / S^1`, and additive integral cohomology ranks; +- named theorem-library facts for Jordan separation on `S^2` and `(R^n)^+ ~= S^n` one-point compactification. + +The additive cohomology ranks of positive-dimensional odd and even spheres are deliberately **not** distinguished: both have rank one in degrees 0 and n and zero elsewhere. Parity appears here through Euler characteristic. + +## Executable-coordinate boundary + +`ExactRealVector n` uses integer coordinates only so these tests stay exact and avoid choosing a floating-point policy. Such points are ordinary points of `R^n`; this is an executable sample subdomain, not a claim that real coordinates are integers. The eventual scalar layer can widen this while keeping the dimension indices and structural constraints. + +Likewise, the quaternion executable fixture uses integer coefficients. It checks Hamilton multiplication and exact norm-one samples without pretending to enumerate the full `S^3` of unit quaternions. + +## OPEN / later passes + +- the general real scalar abstraction and precision policy; +- arbitrary-axis Householder reflections and general-angle Givens rotations; +- concrete matrix realization and determinant/orthogonality checking for imported matrices; +- subspaces, orthogonal projection, and projection-law certificates; +- normalized arbitrary semantic embeddings and cosine similarity; +- a genuine quotient representation for `CP^n` rather than only typed standard facts; +- the cohomology ring `Z[x]/(x^(n+1))`, `|x| = 2`, rather than only additive ranks; +- full theorem provenance/explanation traces in the elaborator. + +The theorem-shaped entries in this slice are not presented as compiler-generated proofs. They model the intended #42 boundary: a checked/versioned mathematical knowledge layer may contribute a named fact when its hypotheses match, and inference should be able to say exactly which fact it used. diff --git a/examples/linear-geometry-type-core/Tests.idric b/examples/linear-geometry-type-core/Tests.idric new file mode 100644 index 0000000000..f861e967f6 --- /dev/null +++ b/examples/linear-geometry-type-core/Tests.idric @@ -0,0 +1,175 @@ +module Tests + +import LinearGeometryTypes + +%default total + +-- -------------------------------------------------------------------------- +-- 1. Dimension-indexed linear algebra +-- -------------------------------------------------------------------------- + +same_dimension_difference_test : + difference + (VCons 5 (VCons 7 VNil)) + (VCons 2 (VCons 3 VNil)) + = VCons 3 (VCons 4 VNil) +same_dimension_difference_test = Refl + +three_four_norm_test : + squaredNorm (VCons 3 (VCons 4 VNil)) = 25 +three_four_norm_test = Refl + +same_dimension_distance_test : + squaredDistance + (VCons 5 (VCons 7 VNil)) + (VCons 2 (VCons 3 VNil)) + = 25 +same_dimension_distance_test = Refl + +explicit_threshold_accepts_test : + withinSquaredTolerance 25 + (VCons 5 (VCons 7 VNil)) + (VCons 2 (VCons 3 VNil)) + = True +explicit_threshold_accepts_test = Refl + +explicit_threshold_rejects_test : + withinSquaredTolerance 24 + (VCons 5 (VCons 7 VNil)) + (VCons 2 (VCons 3 VNil)) + = False +explicit_threshold_rejects_test = Refl + +semantic_residual_test : + semanticResidual + (Embedding (VCons 5 (VCons 7 VNil))) + (Embedding (VCons 2 (VCons 3 VNil))) + = VCons 3 (VCons 4 VNil) +semantic_residual_test = Refl + +-- A differently dimensioned pair is intentionally not representable as an +-- argument to difference/semanticResidual. Dimension agreement is a type +-- constraint, not a runtime convention. + +-- -------------------------------------------------------------------------- +-- 2. O(n), SO(n), reflections, and a first exact Givens-style quarter turn +-- -------------------------------------------------------------------------- + +orientation_reflection_reflection_test : + composeOrientation Reversing Reversing = Preserving +orientation_reflection_reflection_test = Refl + +orientation_rotation_reflection_test : + composeOrientation Preserving Reversing = Reversing +orientation_rotation_reflection_test = Refl + +reflection_in_r3_type_test : OrthogonalTransform 3 Reversing +reflection_in_r3_type_test = firstAxisReflection + +quarter_turn_in_r3_type_test : SpecialOrthogonal 3 +quarter_turn_in_r3_type_test = firstPlaneQuarterTurn + +two_reflections_land_in_so3_test : SpecialOrthogonal 3 +two_reflections_land_in_so3_test = + twoReflections firstAxisReflection firstAxisReflection + +-- -------------------------------------------------------------------------- +-- 3. Spheres: ambient dimension is carried by the type and O(n) preserves it +-- -------------------------------------------------------------------------- + +north_pole_is_s2_test : UnitSpherePoint 2 +north_pole_is_s2_test = northPoleS2 + +so3_action_stays_on_s2_test : UnitSpherePoint 2 +so3_action_stays_on_s2_test = + actSOOnUnitSphere firstPlaneQuarterTurn northPoleS2 + +sphere_s0_h0_rank_test : + sphereIntegralCohomologyRank 0 0 = 2 +sphere_s0_h0_rank_test = Refl + +sphere_s2_h0_rank_test : + sphereIntegralCohomologyRank 2 0 = 1 +sphere_s2_h0_rank_test = Refl + +sphere_s2_h1_rank_test : + sphereIntegralCohomologyRank 2 1 = 0 +sphere_s2_h1_rank_test = Refl + +sphere_s2_h2_rank_test : + sphereIntegralCohomologyRank 2 2 = 1 +sphere_s2_h2_rank_test = Refl + +odd_sphere_euler_test : + sphereEulerCharacteristic 3 = 0 +odd_sphere_euler_test = Refl + +even_sphere_euler_test : + sphereEulerCharacteristic 4 = 2 +even_sphere_euler_test = Refl + +-- -------------------------------------------------------------------------- +-- 4. Quaternions and the unit-quaternion -> SO(3) boundary +-- -------------------------------------------------------------------------- + +quaternion_i_j_test : + quaternionMultiply quatI quatJ = quatK +quaternion_i_j_test = Refl + +quaternion_j_i_test : + quaternionMultiply quatJ quatI = quaternionNegate quatK +quaternion_j_i_test = Refl + +quaternion_i_norm_test : + quaternionNormSquared quatI = 1 +quaternion_i_norm_test = Refl + +unit_quaternion_rotation_is_so3_test : SpecialOrthogonal 3 +unit_quaternion_rotation_is_so3_test = quaternionRotation unitQuatI + +-- -------------------------------------------------------------------------- +-- 5. CP^n and standard quotient/cohomology facts +-- -------------------------------------------------------------------------- + +cp3_real_dimension_test : + cpRealDimension 3 = 6 +cp3_real_dimension_test = Refl + +cp3_hopf_sphere_dimension_test : + cpHopfSphereDimension 3 = 7 +cp3_hopf_sphere_dimension_test = Refl + +cp2_h0_rank_test : + cpIntegralCohomologyRank 2 0 = 1 +cp2_h0_rank_test = Refl + +cp2_h2_rank_test : + cpIntegralCohomologyRank 2 2 = 1 +cp2_h2_rank_test = Refl + +cp2_h4_rank_test : + cpIntegralCohomologyRank 2 4 = 1 +cp2_h4_rank_test = Refl + +cp2_h3_rank_test : + cpIntegralCohomologyRank 2 3 = 0 +cp2_h3_rank_test = Refl + +cp2_h6_rank_test : + cpIntegralCohomologyRank 2 6 = 0 +cp2_h6_rank_test = Refl + +-- -------------------------------------------------------------------------- +-- 6. Named standard topology facts: do not make inference rediscover proofs +-- -------------------------------------------------------------------------- + +jordan_curve_has_two_complement_components_test : + complementComponentCount (jordanSeparation jordanCurveExample) = 2 +jordan_curve_has_two_complement_components_test = Refl + +r3_one_point_compactifies_to_s3_test : + compactifiedSphereDimension (euclideanOnePointCompactification 3) = 3 +r3_one_point_compactifies_to_s3_test = Refl + +main : IO () +main = putStrLn "linear geometry type core: ok" diff --git a/tests/idris2/basic/edric008/expected b/tests/idris2/basic/edric008/expected new file mode 100644 index 0000000000..2f7f178756 --- /dev/null +++ b/tests/idris2/basic/edric008/expected @@ -0,0 +1 @@ +linear geometry type core: ok diff --git a/tests/idris2/basic/edric008/run b/tests/idris2/basic/edric008/run new file mode 100644 index 0000000000..5167626c5b --- /dev/null +++ b/tests/idris2/basic/edric008/run @@ -0,0 +1,7 @@ +. ../../../testutils.sh + +cp ../../../../examples/linear-geometry-type-core/LinearGeometryTypes.idric LinearGeometryTypes.idr +cp ../../../../examples/linear-geometry-type-core/Tests.idric Tests.idr + +"$idris2" Tests.idr -o linear-geometry-type-core >/dev/null +./build/exec/linear-geometry-type-core