Module Synapx.LF

Approximate LF Syntax

type 'a ctx = 'a Synint.LF.ctx =
  1. | Empty
  2. | Dec of 'a ctx * 'a
type svar_class = Synint.LF.svar_class =
  1. | Ren
  2. | Subst
type kind =
  1. | Typ
  2. | PiKind of typ_decl * Syncom.Depend.t * Syncom.Plicity.t * kind
and typ_decl =
  1. | TypDecl of Syncom.Name.t * typ
  2. | TypDeclOpt of Syncom.Name.t
and cltyp =
  1. | MTyp of typ
  2. | PTyp of typ
  3. | STyp of svar_class * dctx
and ctyp =
  1. | ClTyp of cltyp * dctx
  2. | CTyp of Syncom.Id.cid_schema
and ctyp_decl =
  1. | Decl of Syncom.Name.t * ctyp * Syncom.Plicity.t
  2. | DeclOpt of Syncom.Name.t
and typ_rec =
  1. | SigmaLast of Syncom.Name.t option * typ
  2. | SigmaElem of Syncom.Name.t * typ * typ_rec
and tuple =
  1. | Last of normal
  2. | Cons of normal * tuple
and normal =
  1. | Lam of Syncom.Location.t * Syncom.Name.t * normal
  2. | Root of Syncom.Location.t * head * spine
  3. | LFHole of Syncom.Location.t * string option
  4. | Tuple of Syncom.Location.t * tuple
  5. | Ann of Syncom.Location.t * normal * typ
and head =
  1. | BVar of Syncom.Id.offset
  2. | Const of Syncom.Id.cid_term
  3. | MVar of cvar * sub option
  4. | Proj of head * proj
  5. | Hole
  6. | PVar of cvar * sub option
  7. | FVar of Syncom.Name.t
  8. | FMVar of Syncom.Name.t * sub option
  9. | FPVar of Syncom.Name.t * sub option
and proj =
  1. | ByPos of int
  2. | ByName of Syncom.Name.t
and spine =
  1. | Nil
  2. | App of normal * spine
and sub =
  1. | EmptySub
  2. | Id
  3. | Dot of front * sub
  4. | SVar of cvar * sub option
  5. | FSVar of Syncom.Name.t * sub option
and front =
  1. | Head of head
  2. | Obj of normal
and cvar =
  1. | Offset of Syncom.Id.offset
  2. | MInst of Int.LF.clobj * Int.LF.ctyp
and dctx =
  1. | Null
  2. | CtxVar of ctx_var
  3. | DDec of dctx * typ_decl
  4. | CtxHole
and ctx_var =
  1. | CtxName of Syncom.Name.t
  2. | CtxOffset of Syncom.Id.offset
and mctx = ctyp_decl ctx
and sch_elem =
  1. | SchElem of typ_decl ctx * typ_rec
and schema =
  1. | Schema of sch_elem list
and psi_hat = Int.LF.ctx_var option * Syncom.Id.offset
and mfront =
  1. | ClObj of dctx * sub
    (*

    Either a contextual term, plain substitution or renaming substitution.

    *)
  2. | CObj of dctx
    (*

    Context meta-object.

    *)