Skip to content

Instantly share code, notes, and snippets.

@okram
Created Oct 11, 2020
Embed
What would you like to do?
mmlang> :[model,mm][define,tree<=[?0|(int;tree;int)]]
==>_[define,tree<=_[_{?}<=_[is,bool<=_[a,0]]|(int;tree;int)]]
mmlang> 0 => tree
==>tree:0
mmlang> 1 => tree
language error: 1 is not a tree
mmlang> (1;0;1) => tree
==>tree:(1;tree:0;1)
mmlang> (1;(2;0;2);1) => tree
==>tree:(1;tree:(2;tree:0;2);1)
mmlang> (1;(2;(3;0;3);2);1) => tree
==>tree:(1;tree:(2;tree:(3;tree:0;3);2);1)
mmlang> (1;(2;(3;(4;0;4);3);2);1) => tree
==>tree:(1;tree:(2;tree:(3;tree:(4;tree:0;4);3);2);1)
mmlang> (1;(2;(3;(4;0;'a');3);2);1) => tree
language error: (1;(2;(3;(4;0;'a');3);2);1) is not a tree
@okram
Copy link
Author

okram commented Oct 11, 2020

Above is recursive types and below is dependent recursive types.

[define,tree<=[?0|(int:x;tree;int:y)[is,x>y]]]
mmlang> (1;0;1) => tree
language error: (1;0;1) is not a tree
mmlang> (3;0;1) => tree
==>tree:(3;tree:0;1)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment