anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-26 17:13:35 +03:00
Code Issues Projects Releases Wiki Activity

[test] remove qualified-by-type constructors

Browse Source
This commit is contained in:
Jan Mas Rovira 2022-01-21 09:20:27 +01:00
parent b808a03760
commit 0d14e62a4f
1 changed files with 8 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
test/Parsing/Test.hs
View File

@ -54,11 +54,6 @@ inductive Empty {};
-- An inductive type named Unit with only one constructor.
inductive Unit { tt : Unit; };
inductive Nat' : Type
{ zero : Nat' ;
suc : Nat' -> Nat' ;
};
-- The use of the type `Type` below is optional.
-- The following declaration is equivalent to Nat'.
@ -86,8 +81,8 @@ inductive Fin (n : Nat) {
-- The type of sized vectors.
inductive Vec (n : Nat) (A : Type)
{
zero : Vec Nat.zero A;
succ : A -> Vec n A -> Vec (Nat.succ n) A;
zero : Vec zero A;
succ : A -> Vec n A -> Vec (succ n) A;
};
-- * Indexed inductive type declarations.
@ -151,8 +146,8 @@ f' := \ {zero ↦ a ; -- We can use lambda abstractions to pattern match
-- signature is missing.
g : Nat -> A;
g Nat.zero := a;
g (Nat.suc t) := a';
g zero := a;
g (suc t) := a';
-- For pattern-matching, the symbol `_` is the wildcard pattern as in
-- Haskell or Agda. The following function definition is equivalent to
@ -176,8 +171,8 @@ neg := A -> Empty;
-- An equivalent type for sized vectors.
Vec' : Nat -> Type -> Type;
Vec' Nat.zero A := Unit;
Vec' (Nat.suc n) A := A -> Vec' n A;
Vec' zero A := Unit;
Vec' (suc n) A := A -> Vec' n A;
--------------------------------------------------------------------------------
-- Fixity notation similarly as in Agda or Haskell.
@ -185,8 +180,8 @@ Vec' (Nat.suc n) A := A -> Vec' n A;
infixl 10 + ;
+ : Nat → Nat → Nat ;
+ Nat.zero m := m;
+ (Nat.suc n) m := Nat.suc (n + m) ;
+ zero m := m;
+ (suc n) m := suc (n + m) ;
--------------------------------------------------------------------------------
-- Quantities for variables.