Commit f5528229 authored by Ralf Jung's avatar Ralf Jung
Browse files

TODO

parent b749d1ca
...@@ -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.
......
Markdown is supported
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