liesnikov

Ltac destruct_fun_explicit T t f :=
  match goal with
  | |- ?G => let Fn := fresh in
            let Hn := fresh in
            let En := fresh in
            enough (forall x : T, G) as Hn;
            [ apply Hn; exact t
            | intros Fn; pose (ap := f Fn);
              destruct Fn; destruct ap eqn: En; subst ap
            ]

liesnikov

let
  defpkgs = builtins.fetchTarball {
    # Descriptive name to make the store path easier to identify
    name = "nixos-22.05.1271.babb041b716";
    # Commit hash for nixos-unstable as of 2018-09-12
    url = "https://releases.nixos.org/nixos/22.05-small/nixos-22.05.1271.babb041b716/nixexprs.tar.xz";
    # Hash obtained using `nix-prefetch-url --unpack <url>`
    sha256 = "0g8vwni83zn6kgkczrm5vwmyhl473rrs9d4k4hn5gfbgfsyv7ls8";
  };
in

liesnikov

{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}

import qualified Unbound.Generics.LocallyNameless as Unbound
import           GHC.Generics (Generic)
import           Control.DeepSeq (NFData, force)

type LName = Unbound.Name LTerm

data LTerm
  = -- | variables  `x`

liesnikov

doesn't work just yet

Links

1. https://lists.gnu.org/archive/html/emacs-orgmode/2018-06/msg00169.html
2. https://kitchingroup.cheme.cmu.edu/blog/2017/04/09/A-better-return-in-org-mode/
3. https://emacs.stackexchange.com/questions/30248/automatically-create-checkbox-in-new-line