小编Hex*_*irp的帖子

a -> m bfrom to函数m (a -> b)在编程中很少出现，但可以在 Reader monad 中制作。以下代码是暂定的实现。这样的图书馆存在吗？

class Monad m => MonadShift m where
  shift :: (a -> m b) -> m (a -> b)

instance MonadShift Identity where
  shift f = Identity (\x -> runIdentity (f x))

instance MonadShift m => MonadShift (ReaderT r m) where
  shift f = ReaderT (\r -> shift (\x -> runReaderT (f x) r))

Coq标准库有两种单位类型。True键入一个Prop，并具有一个构造函数I : True。另一个unit是输入的Set，并且具有单个构造函数tt : unit。我不知道什么是名称的由来I和tt。

$ coqtop -nois
Welcome to Coq 8.7.0 (October 2017)

Coq < Ltac i := idtac.
Toplevel input, characters 0-4:
> Ltac i := idtac.
> ^^^^
Error: Syntax error: illegal begin of vernac.

我正在"coqtop -nois"下重新开发"Coq.Init.Prelude"和"HoTT.Basics.Overture"进行实践.我发现很难直接写表达式.这就是我想要使用战术的原因.我想知道为什么我不能使用"Ltac".