Commit b6140c48 authored by Sven Wille's avatar Sven Wille

more partial functions (corrected)

parent 74f9cbc6
......@@ -5,7 +5,7 @@ import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory FinSequences : base:?Logic =
include arith:?NaturalArithmetics ❙
include arith:?RealArithmetics ❙
below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n ⟩ ❙
// toBelow : {n : ℕ} below (Succ n) ❘# toB 1❙
// succBelow : {n : ℕ} below n ⟶ below (Succ n) ❘# succB 2❙
......@@ -38,5 +38,5 @@ theory FinSequences : base:?Logic =
// belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)❙
// belowShift_base : {n, b} ⊦ belowShift n 0 b ≐ b❙
// finSeqSum : {n : ℕ , b : below n}
finSeqSum : {n : ℕ} finSeq n ℝ ⟶ ℝ
......@@ -3,7 +3,7 @@ import base http://mathhub.info/MitM/Foundation ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import sub http://gl.mathhub.info/MMT/LFX/Subtyping ❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
// SW this file is mainly for documentation purposes on different ways on how to implement partial functions ❚
theory partialFunctions1 : base:?Logic =
// SW simple version of partial functions using the option type. the disadvantage of this version is that one has
......@@ -36,19 +36,19 @@ theory partialFunctions4 : base:?Logic =
theory partialFunctions5 : base:?Logic =
include ts:?TypedSets ❙
include sub:?LFSubtyped
include sig:?LFSigma
// SW this version make partialFuncions a subtype of normal functions (I think it should be the other way arround , but thats not possible)
and forces that the function throws away the proof argument
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] ⟨ f : {v : d} ⊦ s v ⟶ c | ⊦ ∃ [fn] f ≐ ([x,y] fn x) ⟩
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] Σ f : ({v : d} ⊦ s v ⟶ c) . ⊦ ∃ [fn] f ≐ ([x,y] fn x)
theory partialFunctions6 : base:?Logic =
include ts:?TypedSets ❙
include sub:?LFSubtyped
include sig:?LFSigma
// SW this version basically enforces via the type waht version 2 need explicitely❙
partialFunction : {d : type} (d ⟶ bool) ⟶ type ⟶ type ❘ = [d,p,r] ⟨ x : d | ⊦ p x ⟩ ⟶ r ❙
partialFunction : {d : type} (d ⟶ bool) ⟶ type ⟶ type ❘ = [d,p,r] (Σ x : d . ⊦ p x) ⟶ r ❙
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