adrianparvino

;; Package-Requires: ((request "0.3.2"))
(require 'request)

(defmacro access (trail value)
  (let ((trail_ (reverse trail))
        (result value))
    (dolist (focus trail_ result)
      (pcase focus
        (`(vector . ,index) (setq result `(aref ,result ',index)))
        (`(object . ,key) (setq result `(alist-get ',key ,result)))))))

lukaszlew

-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html
import Data.List (delete, union)
{- HLINT ignore "Eta reduce" -}

-- File mnemonics:
--   env = typing environment
--   vid = variable identifier in Bind or Var
--   br = binder variant (Lambda or Pi)
--   xyzTyp = type of xyz
--   body = body of Lambda or Pi abstraction