Mercurial > cpdt > repo
diff src/Equality.v @ 568:81d63d9c1cc5
Port to Coq 8.9.0
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Jan 2019 15:16:29 -0500 |
parents | d65e9c1c9041 |
children | 0ce9829efa3b |
line wrap: on
line diff
--- a/src/Equality.v Sun Jan 20 15:00:32 2019 -0500 +++ b/src/Equality.v Sun Jan 20 15:16:29 2019 -0500 @@ -214,7 +214,7 @@ end. End fhlist. -Implicit 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. - Implicit Arguments fhmap [ls]. + Arguments fhmap [ls]. (* begin hide *) (* begin thide *) @@ -496,7 +496,7 @@ | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2) end. - Implicit Arguments fhapp [ls1 ls2]. + Arguments fhapp [ls1 ls2]. (* EX: Prove that fhapp is associative. *) (* begin thide *) @@ -676,7 +676,7 @@ (* end thide *) End fhapp. -Implicit 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. *)