# IRC log for #isabelle, 2016-11-03

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
15:46 JCaesar btw, what is different when I declare a function to be (sequential)?
17:03 ThreeOfEight JCaesar: pattern matching is sequential
17:03 ThreeOfEight i.e. the patterns may overlap, and if they do, the earlier equations take precedence over the later ones (like in Haskell, ML, etc)
17:04 ThreeOfEight without "sequential", something like "f 0 = …"  | "f x = …" would not be allowed because of f erlap
17:04 ThreeOfEight *because of overlap
17:04 ThreeOfEight "fun" has that switched on by default
17:04 ThreeOfEight "function" does not
17:04 JCaesar ty
17:38 JCaesar Oh, and btw, another question: I'd like to have an unfold/simplification of the form A + ({# B #} + C) = {# B #} + (A + C). Somehow, I have to prevent that from being applicable if A is of the form {# _ #}. Is there some way to do that?
17:56 ThreeOfEight well you can use a NO_MATCH
17:57 ThreeOfEight define the simp rule with precondition "NO_MATCH {# x #} A"
17:57 ThreeOfEight or possibly "NO_MATCH A {# x #}"
17:57 ThreeOfEight I can never remember the order
17:57 ThreeOfEight any particular reason why you want to prevent that?
17:58 ThreeOfEight it shouldn't ordinarily cause looping because I think the simplifier should recognise this as a permutative rewrite rule
17:59 JCaesar maybe I broke that recognition somehow…