Fixed argumentless constructors being treated as variables.

This commit is contained in:
Samuel Hammersberg 2023-03-28 13:50:19 +02:00
parent d7549d421c
commit 2aff7a7743
3 changed files with 56 additions and 67 deletions

View file

@ -1,26 +1,20 @@
data Maybe () where {
Nothing : Maybe ()
Just : Int -> Maybe ()
data List () where {
Nil : List ()
Cons : Int -> List () -> List ()
};
-- fmap : (Int -> Int) -> Maybe () -> Maybe () ;
-- fmap f ma = case ma of {
-- Nothing => Nothing ;
-- Just a => Just (f a) ;
-- };
main = case (Just 10) of {
Just a => a ;
Nothing => 1 ;
main = case Nil of {
Nil => 0 ;
Cons a _ => a ;
};
-- pure : Int -> Maybe () ;
-- pure x = Just x ;
--
-- return = pure;
--
-- bind : Maybe () -> (Int -> Maybe ()) -> Maybe () ;
-- bind ma f = case ma of {
-- Nothing => Nothing ;
-- Just a => f a ;
-- length : List () -> Int ;
-- length xs = case xs of {
-- Nil => 0;
-- Cons _ xs => 1 + length xs ;
-- };
--sum xs = case xs of {
-- Nil => 0 ;
-- Cons a xs => a + main xs ;
--};