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

Safe Haskell | Safe-Infered

Agda.TypeChecking.CompiledClause

# Documentation

type :-> key value = Map key value

data Case c

Constructors

Branches |
Fields conBranches :: QName :-> c litBranches :: Literal :-> c catchAllBranch :: Maybe c

Instances

Functor Case |
Typeable1 Case |
Data c => Data (Case c) |
Pretty a => Show (Case a) |
Monoid m => Monoid (Case m) |
Pretty a => Pretty (Case a) |
Abstract a => Abstract (Case a) |
Apply a => Apply (Case a) |
EmbPrj a => EmbPrj (Case a) |
InstantiateFull a => InstantiateFull (Case a) |

data CompiledClauses

Constructors

Case Int (Case CompiledClauses) | `Case n bs` stands for a match on the `n`-th argument (counting from zero) with `bs` as the case branches.
Done [Arg String] Term | `Done xs b` stands for the body `b` where the `xs` contains hiding and name suggestions for the free variables. This is needed to build lambdas on the right hand side for partial applications which can still reduce.
Fail | Absurd case.

Instances

Data CompiledClauses |
Show CompiledClauses |
Typeable CompiledClauses |
Pretty CompiledClauses |
Abstract CompiledClauses |
Apply CompiledClauses |
EmbPrj CompiledClauses |
InstantiateFull CompiledClauses |

litCase :: Literal -> c -> Case c

conCase :: QName -> c -> Case c

catchAll :: c -> Case c