我正在形式化一个语法，它本质上是一个布尔表达式。在 coq 中，您可以在 Prop 或更明确地在 bool 中获得类似布尔值的东西。
例如，我可以这样写：
true && true
或者
True /\ True
问题是，在证明中（这是我真正关心的），我可以在域 bool 中进行案例分析，但在 Prop 中这是不可能的（因为我认为所有成员都不可枚举）。即使对于非常简单的证明，放弃这种策略和类似的重写策略似乎也是一个巨大的缺点。
一般来说，在什么情况下会选择 Prop 而不是 bool 进行形式化？我意识到这是一个广泛的问题，但我觉得 Coq 手册中没有充分解决这个问题。我对人们在两条路线上的真实经历很感兴趣。
我正在使用 Ravenscar 配置文件构建一个利用任务的应用程序。
举一个简单的例子，我有一个任务有一个屏障，因此它仅在屏障为 True 时执行。
但是，我注意到，如果主控制线程正在执行，然后屏障设置为 true（从而释放），则任务将阻止主线程的执行，直到屏障再次关闭。
我正在研究 NRF52840 芯片。我应该注意，每当我将应用程序（没有修改）定位到 Native 时，这个问题就不会发生，并且任务不会阻止执行。
为了在嵌入式设备上启用 ravenscar（完整）RTS 的并行执行，我需要做些什么吗？
一些额外的颜色：如果我向任务循环添加延迟，它确实允许主控制线程运行。
这可能是优先级上限协议的问题吗？板上的处理器只有一个核心，所以我想知道这是否可能是问题所在——也就是说，该任务不允许主任务抢占，除非它正在休眠。
我正在尝试使用数组传递和访问类型做一些事情。我遇到过这样一种情况：嵌入式系统上的堆栈大小使得难以通过典型的参数传递机制传递大型数组。
为了节省堆栈大小，我已经开始使用访问类型，但我不想进行动态分配。
我所拥有的是这样的：
type My_Array_Type is array (Natural range<>) of Integer;
type My_Array_Type_Ptr is access all My_Array_Type;
procedure Do_Stuff(Things : My_Array_Type_Ptr) is
begin
-- things
end Do_Stuff;
procedure Do_Stuff(Num_Things : Integer) is
Things : My_Array_Type_Ptr := new My_Array_Type(1..Num_Things);
begin
Do_Stuff(Things);
-- more things
end Do_Stuff;
但是，我想做的是这样的：
type My_Array_Type is array (Natural range<>) of Integer;
procedure Do_Stuff(Things : access all My_Array_Type) is
begin
-- things
end Do_Stuff;
procedure Do_Stuff(Num_Things : Integer) is
Things : aliased My_Array_Type(1..Num_Things);
begin
Do_Stuff(Things'Access);
-- more things …