owo-lang / minitt-rs Goto Github PK

Contributors

Stargazers

Forkers

mafm binadamu-isiyoonekana

const pattern = value;

sum { True | False }
split { True =>  | False => }

=> :load samples\sum-split\maybe.minitt
=> :gamma
Current Gamma:
maybe: Π _: U. U
the: Π t: U. Π _: t. t
unwrap: Π t: U. Π mt: (maybe t). ((unwrap_type t) mt)
unwrap_type: Π t: U. Π _: (maybe t). U
=> :type unwrap (Just 1)
Cannot infer type of: `Just 1`.
At unknown location.
=> :type unwrap (Just 0)
Cannot infer type of: `Just 0`.
At unknown location.

=>
Parse failed at: --> 1:1
  |
1 |
  | ^---
  |
  = expected expression

let id_on_id: (A: type_t, A) -> A =
  id((A: type_t, A) -> A)(id)

let bool: Type = Sum { True } ++ Sum { False };

let threee: U = sum { One | Two | Three };
let three: U = sum { Two | Three };

let three_f (a: U) (m: three): 1 = split { Two => 0 | Three => 0 };
let threee_f (a: U) (m: threee): 1 = split { One => 0 | e => (three_f a) e };