hiker

  -- ogf(c,x) = Σ n:ℕ, cₙ xⁿ
  def ogf (c : ℕ → ℕ) (α : Type) :=
  Σ n:ℕ, fin (c n) × (fin n → α)

  inductive list (α : Type)
  | nil : list
  | cons (hd : α) (tl : list) : list

  inductive bin_tree (α : Type)
  | leaf : bin_tree
  | branch (x : α) (left : bin_tree) (right : bin_tree) : bin_tree

  int getint(const char **s) {
    int res = 0;
    for (; **s && isspace(**s); (*s)++);
    for (; **s && isdigit(**s); (*s)++)
      res = 10 * res + **s - '0';
    return res;
  }

  data Expr b
    = Var   Id
    | Lit   Literal
    | App   (Expr b) (Arg b)
    | Lam   b (Expr b)
    | Let   (Bind b) (Expr b)
    | Case  (Expr b) b Type [Alt b]
    | Tick  (Tickish Id) (Expr b)
    | Type  Type
    | Cast  (Expr b) Coercion
    | Coercion Coercion

  data Type
    = TyVarTy   Var
    | LitTy     TyLit
    | AppTy     Type Type
    | ForAllTy  !TyCoVarBinder Type
    | FunTy     Type Type
    | TyConApp  TyCon [KindOrType]
    | CastTy    Type KindCoercion
    | CoercionTy Coercion

  inductive expr
  | var         : nat → expr
  | sort        : level → expr
  | const       : name → list level → expr
  | mvar        : name → name → expr → expr
  | local_const : name → name → binder_info → expr → expr
  | app         : expr → expr → expr
  | lam         : name → binder_info → expr → expr → expr
  | pi          : name → binder_info → expr → expr → expr
  | elet        : name → expr → expr → expr → expr
  | macro       : macro_def → list expr → expr