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

Safe HaskellNone

Agda.Compiler.JS.Case

Documentation

data Case Source

Constructors

Case 

Fields

pats :: [Patt]
 
body :: Exp
 

Instances

Show Case 
Pretty Case 

data Patt Source

Constructors

VarPatt 
Tagged Tag [Patt] 

Instances

Show Patt 
Pretty Patt 

data Tag Source

Constructors

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

Instances

Show Tag 

numVars :: [Patt] -> NatSource

numVars' :: Patt -> NatSource

lambda :: [Case] -> ExpSource

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

pop :: Case -> CaseSource

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

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

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

tags :: [Case] -> Map MemberId NatSource

tag :: Case -> Map MemberId NatSource