Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Compiler.JS.Case

# Documentation

data Case

Constructors

Case |
Fields pats :: [Patt] body :: Exp

Instances

Show Case |
Pretty Case |

data Patt

Constructors

VarPatt |
Tagged Tag [Patt] |

Instances

Show Patt |
Pretty Patt |

data Tag

Constructors

Tag MemberId [MemberId] (Exp -> [Exp] -> Exp) |

Instances

Show Tag |

numVars :: [Patt] -> Nat

numVars' :: Patt -> Nat

lambda :: [Case] -> Exp

lambda' :: Nat -> Nat -> Nat -> [Case] -> Exp

pop :: Case -> Case

match :: Nat -> Nat -> Nat -> [Case] -> MemberId -> Nat -> Exp

refine :: MemberId -> Nat -> Case -> [Case]

visit :: [Case] -> Exp -> [Exp] -> Exp

tags :: [Case] -> Map MemberId Nat

tag :: Case -> Map MemberId Nat