Skip to content

GitLab

Commit 58893fc3 authored by Ralf Jung's avatar Ralf Jung
Browse files

TODO

parent eae4cc01
Hide whitespace changes
Inline Side-by-side
prelude/functions.v
View file @ 58893fc3
...@@ -8,7 +8,7 @@ Section definitions. ...@@ -8,7 +8,7 @@ Section definitions.
λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b. λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
End definitions. End definitions.
(* For now, we only have the properties here that do not need a notion (* TODO: For now, we only have the properties here that do not need a notion
of equality of functions. *) of equality of functions. *)
Section functions. Section functions.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment