swift-pterodactyl / examples / test.ptero

// For pedagogical reasons it can be nice to explicitly apply introduction rules.
exampleVerbose : (A : Type) (x : A) -> {tp: Type; elt: tp}
exampleVerbose <= intro 
exampleVerbose A <= intro 
exampleVerbose A x <= intro
exampleVerbose A x .tp => A
exampleVerbose A x .elt => x

singleton : (X : Type) (x : X) -> Type 
singleton X x => {fst : X; snd : x = fst}

reflExample : (X : Type) (x : X) -> singleton X x
reflExample X x <= intro 
reflExample X x .fst => x 
reflExample X x .snd => refl

reflExample (X : Type) (x : X) : singleton X x 
reflExample X x => ?

// But we can also have these applied automatically.
example : (A : Type) (x : A) -> {tp: Type; elt: tp}
example A x .tp => A
example A x .elt => x

foo : Type -> {tp : Type; elt : tp}
foo A => ?