diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-04 13:20:46 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-04 13:20:46 +0100 |
| commit | 29a05f990dd945be30995c4f46b91b5f7c83abd9 (patch) | |
| tree | fc68c964af9d02682520592e4566d25030b47031 /src/Term/Syntax.idr | |
| parent | 8791efda0cf7392144117cf780bfb6d687d2da5e (diff) | |
Make unions a pseudo-built-in type.
Diffstat (limited to 'src/Term/Syntax.idr')
| -rw-r--r-- | src/Term/Syntax.idr | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr index 0ba09a2..d403440 100644 --- a/src/Term/Syntax.idr +++ b/src/Term/Syntax.idr @@ -43,8 +43,23 @@ t `mod` u = App (App (Op Mod) t) u export Arb : {ty : Ty} -> Term ty ctx -Arb {ty = N} = Zero -Arb {ty = ty ~> ty'} = Const Arb +Arb = Op (Arb ty) + +export +inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx +inL = Op (Inl ty1 ty2) + +export +inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx +inR = Op (Inr ty1 ty2) + +export +prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx +prL = Op (Prl ty1 ty2) + +export +prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx +prR = Op (Prr ty1 ty2) -- HOAS |