| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Auto.Syntax

Documentation

data RefInfo o | Source

Constructors

RIEnv [ConstRef o] |
RIMainInfo Nat (HNExp o) |
forall a . RIUnifInfo (Metavar a (RefInfo o)) [CAction o] (HNExp o) |

Instances

Refinable (ArgList o) (RefInfo o)
Refinable (Exp o) (RefInfo o)
Trav (CAction o) (RefInfo o)
Trav (CArgList o) (RefInfo o)
Trav (HNExp o) (RefInfo o)
Trav (ArgList o) (RefInfo o)
Trav (Exp o) (RefInfo o)
Trav ((,) MId (CExp o)) (RefInfo o)
Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o)

type MyPB o = PB (RefInfo o) | Source

type MyMB a o = MB a (RefInfo o) | Source

type Nat = Int | Source

data FMode | Source

Constructors

Hidden |
NotHidden |

Instances

Eq FMode

data MId | Source

Constructors

Id String |
NoId |

data Abs a | Source

Constructors

Abs MId a |

data ConstDef o | Source

Constructors

ConstDef |

cdname :: String |
cdorigin :: o |
cdtype :: MExp o |
cdcont :: DeclCont o |

data DeclCont o | Source

Constructors

Def Nat [Clause o] |
Datatype [ConstRef o] |
Constructor |
Postulate |

type Clause o = ([Pat o], MExp o) | Source

data Pat o | Source

Constructors

PatConApp (ConstRef o) [Pat o] |
PatVar |
PatExp |

type ConstRef o = IORef (ConstDef o) | Source

data Elr o | Source

Constructors

Var Nat |
Const (ConstRef o) |

data Sort | Source

Constructors

SortLevel Nat |
Type |

data Exp o | Source

Constructors

App (Elr o) (MArgList o) |
Lam FMode (Abs (MExp o)) |
Fun FMode (MExp o) (MExp o) |
Pi FMode Bool (MExp o) (Abs (MExp o)) |
Sort Sort |

Instances

Refinable (Exp o) (RefInfo o)
Trav (Exp o) (RefInfo o)

type MExp o = MM (Exp o) (RefInfo o) | Source

data ArgList o | Source

Constructors

ALNil |
ALCons FMode (MExp o) (MArgList o) |
ALConPar (MArgList o) |

Instances

Refinable (ArgList o) (RefInfo o)
Trav (ArgList o) (RefInfo o)

type MArgList o = MM (ArgList o) (RefInfo o) | Source

data HNExp o | Source

Constructors

HNApp (Elr o) (CArgList o) |
HNLam (Abs (CExp o)) |
HNFun FMode (CExp o) (CExp o) |
HNPi FMode Bool (CExp o) (Abs (CExp o)) |
HNSort Sort |

Instances

Trav (HNExp o) (RefInfo o)

data HNArgList o | Source

Constructors

HNALNil |
HNALCons (CExp o) (CArgList o) |
HNALConPar (CArgList o) |

type CExp o = Clos (MExp o) o | Source

data CArgList o | Source

Constructors

CALNil |
CALConcat (Clos (MArgList o) o) (CArgList o) |

Instances

Trav (CArgList o) (RefInfo o)

data Clos a o | Source

Constructors

Clos [CAction o] a |

Instances

Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o)

data CAction o | Source

Constructors

Sub (CExp o) |
Skip |
Weak Nat |

Instances

Trav (CAction o) (RefInfo o)

type Ctx o = [(MId, CExp o)] | Source

type EE = IO | Source

data Elrs o | Source

Constructors

ElrsNil |
ElrsCons (Elr o) (Elrs o) |
ElrsWeak (Elrs o) |

Produced by Haddock version 2.4.2