Stream: Coq users

Topic: Different statements?


view this post on Zulip zohaze (Nov 28 2021 at 13:23):

I have these four hypothesis and non empty list. May I write nth i2 (a::l) 0 >= nth i1 (a::l) 0?

H1 : max a (list_max l) <= a
H2: a <= max a (list_max l).
H3: nth i2 (a :: l) 0 < nth i1 (a :: l) 0
H4: nth (S i2) (a :: l) 0 < nth i1 (a :: l) 0

view this post on Zulip Karl Palmskog (Nov 28 2021 at 13:58):

please use the triple backtick syntax for code fragments, i.e., write three backticks, then a newline and your code, then a newline and three backticks again. For example, like this (you can view the source of this answer)

H1 : max a (list_max l) <= a

also see: https://github.com/adam-p/markdown-here/wiki/Markdown-Cheatsheet#code-and-syntax-highlighting


Last updated: Feb 04 2023 at 23:02 UTC