abenori

--import Binomcoef.Basic
import Mathlib.Tactic
import Mathlib.Tactic.Lift
import Mathlib.Tactic.Ring
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Lift
import Mathlib.Data.Rat.Defs
import Mathlib.Tactic.Qify

abenori

@require: stdja
@require: base/length

let length-to-str len = (Float.to-string (Length.to-float len)) ^ `pt`

let-inline ctx \test =
  let ib = read-inline ctx {X} in
  let (w,h,d) = get-natural-metrics ib in
  let draw (x,y) =
    let gr = 

abenori

@require: stdja
@require: list
@require: base/list-ext
@require: base/length

% \arrow / \crで指定された内容を一時的に格納する
let-mutable ref-arrows <- []
let-mutable ref-cr <- false

% helpers

abenori

local engine = "platex"
local target = "original"

local do_not_use_latex_for_pdf_file = false


local style = "abmrepos"
local lfs = require "lfs"

local latexopt = "-interaction=nonstopmode"

abenori

% -*- coding: utf-8 -*-
@require: pervasives
@require: gr
@require: list
@require: math
@require: color
@require: option
@require: annot