### Site Tools

plt17:assignment_2

# Differences

This shows you the differences between two versions of the page.

 plt17:assignment_2 [2017/12/05 14:43]hossein [Task 3] plt17:assignment_2 [2017/12/05 14:45]hossein [Task 1] Both sides previous revision Previous revision 2017/12/05 14:45 hossein [Task 3] 2017/12/05 14:45 hossein [Task 1] 2017/12/05 14:43 hossein [Task 3] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 12:21 hossein [Task 2] 2017/09/30 23:32 hossein [Task 1] 2017/09/27 00:23 hossein created 2017/12/05 14:45 hossein [Task 3] 2017/12/05 14:45 hossein [Task 1] 2017/12/05 14:43 hossein [Task 3] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 14:42 hossein [Task 1] 2017/12/05 12:21 hossein [Task 2] 2017/09/30 23:32 hossein [Task 1] 2017/09/27 00:23 hossein created Last revision Both sides next revision Line 20: Line 20: A set can be defined using a predicate $P(x)$ that determines if an object belongs to the set or not $\{x | P(x)\}$. ​ A set can be defined using a predicate $P(x)$ that determines if an object belongs to the set or not $\{x | P(x)\}$. ​ Set is a collection of objects for which $P$ is true. Set is a collection of objects for which $P$ is true. - Define the function ''​Fixpoint''​ that gets a variable and determines if it is free in a λ-expression or not. + Define the function ''​free''​ that gets a variable and determines if it is free in a λ-expression or not. - ''​Fixpoint ​Free (x: string) (e: term) : Prop''​. + ''​Fixpoint ​free (x: string) (e: term) : Prop''​. ===== Task 2 ===== ===== Task 2 =====