Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] types problem


view this post on Zulip Email Gateway (Aug 22 2022 at 13:02):

From: Omar Jasim <oajasim1@sheffield.ac.uk>
Hi

please I have problem with understanding the types and how to make
definition for example:

definition prime :: "nat ⇒ bool" where "prime p = (1 < p ∧ (∀m. m dvd
p ⟶ m = 1 ∨ m = p))"

please can any one help me to understand it as I have complex statements.
Many thanks in advance.
Regards
Omar

view this post on Zulip Email Gateway (Aug 22 2022 at 13:03):

From: Jonathan Woodgate via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

problem with understanding the types and how to make definition
can you clarify you question? 

Omar Jasim <oajasim1@sheffield.ac.uk> schrieb am 18:06 Dienstag, 22.März 2016:

Hi

please I have problem with understanding the types and how to make
definition for example:

definition prime :: "nat ⇒ bool"  where "prime p = (1 < p ∧ (∀m. m dvd
p ⟶ m = 1 ∨ m = p))"

please can any one help me to understand it as I have complex statements.
Many thanks in advance.
Regards
Omar


Last updated: Apr 25 2024 at 16:19 UTC