Stream: Coq Workshop 2021

Topic: [S3T1] SSProve


view this post on Zulip Christian Doczkal (Jul 02 2021 at 13:24):

Presentation given by @Théo Winterhalter

view this post on Zulip Christian Doczkal (Jul 02 2021 at 13:34):

@Théo Winterhalter , I was a bit surprised that your external hint for the validity of if _ then _ else _ did not talk about the condition. Does the condition have to be a variable? I guess it can't be an arbitrary program.

view this post on Zulip Théo Winterhalter (Jul 02 2021 at 13:36):

It seems to work as is for conditional of the form

if ek == ek' then ... else ...

view this post on Zulip Théo Winterhalter (Jul 02 2021 at 13:36):

(which we have in our examples)


Last updated: Apr 19 2024 at 02:02 UTC