Commit e10c8ea4 authored by Dennis Müller's avatar Dennis Müller

possible bug(?)

parent 20b587b3
......@@ -64,7 +64,7 @@ theory DirectedSet : base:?Logic =
directedSet = Mod directedSet_theory ❘ role abbreviation ❙
theory Fixpoints : ur:?LF =
theory Fixpoints : base:?Logic =
include ?AllSets ❙
isFixpoint: {A:type, f:A ⟶ A, a:A} prop ❘ = [A,f,a] f a ≐ a ❙
fixpoints: {A:type} (A ⟶ A) ⟶ set A ❘ = [A,f] ι [s] ∀[x] x ∈ s ⇒ isFixpoint A f x ❙
......
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