典型的な依存型システム利用

def FooRetType (b:Bool) : Type :=
match b with
| false => Nat
| true => String

def foo (b: Bool) : FooRetType b :=
 match b with
 | false => (1 : Nat)
 | true => "hello"
#eval foo true
#eval foo false