Commit 6174d946 authored by Max Rapp's avatar Max Rapp

Fix naming

parent 630a79b2
......@@ -65,8 +65,8 @@ theory DirectedSet : base:?Logic =
theory Fixpoints : ur:?LF =
include ?AllSets ❙
is_fixpoint: {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 ⇒ is_fixpoint A f x ❙
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 ❙
theory POSet : base:?Logic =
......
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