anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-11 08:25:46 +03:00
Code Issues Projects Releases Wiki Activity

[ tests ] added example about ordinals

Browse Source
This commit is contained in:
Jonathan Prieto-Cubides 2022-03-08 13:25:17 +01:00
parent 02c17c1d1f
commit 7f501de774
2 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/MiniJuvix/Termination/Types/SizeRelation.hs
View File

@ -61,5 +61,5 @@ instance Pretty Rel where
instance Pretty Rel' where instance Pretty Rel' where
pretty r = case r of pretty r = case r of
REq -> pretty ("∼" :: Text) REq -> pretty ("=" :: Text)
RLe -> pretty ("≺" :: Text) RLe -> pretty ("≺" :: Text)

15
tests/positive/Termination/Data/List.mjuvix
View File

@ -88,4 +88,19 @@ aux A (cons _ x xs) ls := cons A x (aux A xs ls);
flat A (nil _) := nil A; flat A (nil _) := nil A;
flat A (cons _ x xs) := aux A x xs; flat A (cons _ x xs) := aux A x xs;
inductive Ord {
ZOrd : Ord;
SOrd : Ord -> Ord;
Lim : (ℕ -> Ord) -> Ord;
};
addord : Ord -> Ord -> Ord;
aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord);
addord (Zord) y := y;
addord (SOrd x) y := SOrd (addord x y);
addord (Lim f) y := Lim (aux-addord f y);
-- where
aux-addord f y z := addord (f z) y;
end; end;