Commit 615d2dcf authored by Sven Wille's avatar Sven Wille

partial functions 2

parent da66d1f0
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
// 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
to "manually" deal with the option type❙
include fnd:?OptionType ❙
partialFunction : type ⟶ type ⟶ 𝒰 100 ❘= [a,b] a ⟶ Option b❙
theory partialFunctions2 : base:?Logic =
include ts:?TypedSets ❙
// SW not completely correct implementation of partial functions since the argument that holds the proof is not discarded
and could lead to problems in certain cases ❙
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❘# { 1 ;; 2 } ⟶p 3 ❙
theory partialFunctions3 : base:?Logic =
include ts:?TypedSets ❙
// SW I think this one leads to problems when used with finite types.
this version is basically translated from isabelle/hol (found in HOL.thy) ❙
undefined : {a : type} a ❙
paritalFunction : { a : type } set a ⟶ type ⟶ type ❘ = [a,s,b] ⟨ f : s ⟶ a ⟶ b | ⊦ ∃ P f = ([ss,v] ) ⟩❙
theory partialFunctions4 : base:?Logic =
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❘# { 1 ;; 2 } ⟶p 3 ❙
theory partialFunctions4 : base:?Logic =
partialFunction : {d : type} set d ⟶ type ⟶ type ❘ = [d,s,c] {v : d} ⊦ s v ⟶ c ❘# { 1 ;; 2 } ⟶p 3 ❙
// set as type version
// use sigma types with special Notation to make it more feel like a normal lf function ❚
// use of subtype
// use subset with proof ❚
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
// this file is mainly for documentation purposes on different ways on how to implement partial functions ❚
theory partialFunctions1 : base:?Logic =
include fnd:?OptionType ❙
a : type ❙
bla : 𝒰 100 ❘ = Option a ❙
partialFunction : type ⟶ type ⟶ 𝒰 100 ❘= [a,b] a ⟶ Option b❙
theory partialFunctions2 : base:?Logic =
include ts:?TypedSets ❙
partialFunction : type ⟶ type ⟶ type ❘ = [d,c] {' domain : set d , f : d ⟶ c'} ❘ # 1 →p 2❙
getDomain : {a : type} {b : type} partialFunction a b ⟶ set a❙
applyPartialFunction : {d : type} {c : type} d →p c ⟶ ❙
theory partialFunctions3 : base:?Logic =
// use arbitary ❙
// u se sigme ❚
// use subset with proof ❚
\ No newline at end of file
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