{"size": 505, "ext": "scrbl", "max_stars_repo_path": "scribblings/sample.scrbl", "max_stars_repo_name": "dedbox/racket-texmath", "max_stars_repo_stars_event_min_datetime": "2018-02-27T04:17:10.000Z", "max_stars_repo_stars_event_max_datetime": "2020-03-08T07:24:42.000Z", "max_issues_repo_path": "scribblings/sample.scrbl", "max_issues_repo_name": "dedbox/racket-texmath", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "scribblings/sample.scrbl", "max_forks_repo_name": "dedbox/racket-texmath", "max_forks_repo_forks_event_min_datetime": "2018-03-25T23:12:09.000Z", "max_forks_repo_forks_event_max_datetime": "2018-03-25T23:12:09.000Z"}
{"max_stars_count": 4, "max_issues_count": null, "max_forks_count": 1, "avg_line_length": 15.303030303, "max_line_length": 52, "alphanum_fraction": 0.3247524752}
#lang scribble/base

@(require texmath)

@inferrule[
      @${e_1 ↝ e_1'}
  ---------------------- "E-App1"
  @${e_1 e_2 ↝ e_1' e_2}
]

@inferrule[
  --------------------------------------- "E-AppAbs"
  @${(λx_11.e_12) v_2 ↝ [x_11↦{}v_2]e_12}
]

@inferrule[
  @${x \fresh}
  ---------------------------- "E-Def"
  @${Σ ⊢ x←v ↝ [x{}↦{}v]Σ ⊢ Ø}
]

@inferrule[
           @${Σ(x) = v}
  ---------------------
  @${Σ,Γ ⊢ x ↝ Σ,Γ ⊢ v}
]

@inferrule[
  @${\{x:T\} ∈ Γ}
  --------------- "T-Var"
  @${<Γ;x>:T}
]
