Mercurial > cpdt > repo
diff src/Equality.v @ 569:0ce9829efa3b
Back to working in Coq 8.4
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Jan 2019 15:28:23 -0500 |
parents | 81d63d9c1cc5 |
children |
line wrap: on
line diff
--- a/src/Equality.v Sun Jan 20 15:16:29 2019 -0500 +++ b/src/Equality.v Sun Jan 20 15:28:23 2019 -0500 @@ -214,7 +214,7 @@ end. End fhlist. -Arguments fhget [A B elm ls]. +Arguments fhget [A B elm ls] _ _. (* begin hide *) (* begin thide *) @@ -235,7 +235,7 @@ | _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls)) end. - Arguments fhmap [ls]. + Arguments fhmap [ls] _. (* begin hide *) (* begin thide *) @@ -496,7 +496,7 @@ | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) end. - Arguments fhapp [ls1 ls2]. + Arguments fhapp [ls1 ls2] _ _. (* EX: Prove that fhapp is associative. *) (* begin thide *) @@ -676,7 +676,7 @@ (* end thide *) End fhapp. -Arguments fhapp [A B ls1 ls2]. +Arguments fhapp [A B ls1 ls2] _ _. (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics. The next section explores an alternative that leads to simpler developments in some cases. *)