如何使用理解或LAMBDA功能获得集合中的最小长度元素
出于某种目的，我想在（'列表集）中获取最小的元素，将整个设置作为最终状态。
但是我不知道如何实现此功能和证明。
definition initState :: "v list set\<Rightarrow> 'v list set" where
"initState vset = {x. x\<in>vset \<and> length x \<le> 1}"
此代码是错误的。
For some purpose, I want to get the smallest length of element in ('a list set) as the InitalState, and the whole set as the FinalState.
But I don't know how to achieve this function and proof.
definition initState :: "v list set\<Rightarrow> 'v list set" where
"initState vset = {x. x\<in>vset \<and> length x \<le> 1}"
This code is wrong.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
首先，找出最小的长度。
定义“ Minlenvset®最小值（长度`vset）”
如果您的设置可以是无限的，则使用INF而不是最大。
挑选一个最小长度元素
然后使用描述（ @或eps）定义
。描述可能很棘手。
First, find out what the smallest length is.
definition "minlen vset ≡ Min (length ` vset)"
Use Inf instead of Max if your set can be infinite.
Then pick out a minimum-length element using a description (@ or Eps)
definition "initState vset ≡ @x. x∈vset ∧ length x = minlen vset"
I suspect there may be a better way to define your state space, however: descriptions can be tricky to work with.