Skip to content
Permalink
Browse files

Changed notation from [+] to [+ₒ] for ordinal successors.

  • Loading branch information...
rlepigre committed Mar 14, 2019
1 parent de45c90 commit 34b595ea0357032b9935907bca3ff3d6847c7cd3
@@ -77,6 +77,7 @@
("\\m" ) ("\\mu" )
("\\n" ) ("\\nu" )
("\\8" ?∞) ("\\infty" ?∞)
("+_o" ["+ₒ"])
;; ("\\v" ?↓) ("\\downarrow" ?↓)
;; ("\\ni" ?∉) ("\\notin" ?∉)
;; ("\\<" ?⊂) ("\\subset" ?⊂)
@@ -36,6 +36,7 @@ syntax match Keyword "\^"
syntax match Keyword ""
syntax match Keyword ""
syntax match Keyword ""
syntax match Keyword "+ₒ"

" Constructors
syntax match Constant "\<\u\w*\>"
@@ -101,6 +102,7 @@ command! -nargs=+ ABBackslashEat call s:DefABEat(<f-args>)
ab -> →
ab => ⇒
ab * ×
ab +o +

" Abbreviations starting with backslash.
ABBackslashEat langle ⟨
@@ -13,7 +13,7 @@ val d2i : digit ⇒ int = fun n {
}
}

val rec average' : ∀s, int ⇒ sinter⟨s+1⟩ ⇒ sinter⟨s+1⟩ ⇒ sinter⟨s⟩ =
val rec average' : ∀s, int ⇒ sinter⟨s+ₒ1⟩ ⇒ sinter⟨s+ₒ1⟩ ⇒ sinter⟨s⟩ =
fun c a b _ {
let (a0,a') = a {};
let (b0,b') = b {};
@@ -30,7 +30,7 @@ val rec average' : ∀s, int ⇒ sinter⟨s+1⟩ ⇒ sinter⟨s+1⟩ ⇒ sinter
}
}

val average : ∀s, sinter⟨s+1⟩ ⇒ sinter⟨s+1⟩ ⇒ sinter⟨s⟩ = average' Zero
val average : ∀s, sinter⟨s+ₒ1⟩ ⇒ sinter⟨s+ₒ1⟩ ⇒ sinter⟨s⟩ = average' Zero

val oppD : digit ⇒ digit = fun d {
case d {
@@ -167,12 +167,12 @@ include lib.either
// either return n with a sized type less or equal than the size of m
// or return n - S[m] with a sized type less that the size of n

val rec sub_size : ∀o1 o2, ∀n∈nat^(o1+1), ∀m∈[S of nat^o2],
val rec sub_size : ∀o1 o2, ∀n∈nat^(o1+ₒ1), ∀m∈[S of nat^o2],
either⟨n∈nat^o2 | n < m, {p∈nat^o1 | n ≡ m + p}⟩ =
fun n m {
case m {
S[m'] →
let rec sub_aux : ∀o1 o2, ∀n∈nat^(o1+1), ∀m∈nat^o2,
let rec sub_aux : ∀o1 o2, ∀n∈nat^(o1+ₒ1), ∀m∈nat^o2,
either⟨n∈nat^o2 | n < S[m], {p∈nat^o1 | n ≡ S[m] + p}⟩ =
fun n m {
case n {
@@ -6,18 +6,18 @@ val head : ∀a, stream⟨a⟩ ⇒ a =
fun s { (s {}).hd }

// Tail of a stream.
val tail : ∀a, ∀s, stream^(s+1)⟨a⟩ ⇒ stream^s⟨a⟩ =
val tail : ∀a, ∀s, stream^(s+ₒ1)⟨a⟩ ⇒ stream^s⟨a⟩ =
fun s { (s {}).tl }

// Head and tail of a string together.
val get : ∀a, ∀s, stream^(s+1)⟨a⟩ ⇒ a × stream^s⟨a⟩ =
val get : ∀a, ∀s, stream^(s+ₒ1)⟨a⟩ ⇒ a × stream^s⟨a⟩ =
fun s {
let {hd; tl} = s {};
(hd, tl)
}

// Construction function.
val cons : ∀a, ∀s, a ⇒ stream^s⟨a⟩ ⇒ stream^(s+1)⟨a⟩ =
val cons : ∀a, ∀s, a ⇒ stream^s⟨a⟩ ⇒ stream^(s+ₒ1)⟨a⟩ =
fun hd tl _ { {hd; tl} }

// Build a stream containing only the given element.
@@ -517,7 +517,7 @@ let parser expr @(m : mode) =
when m <<= Ord E
-> in_pos _loc EConv
(* Ordinal (successor) *)
| o:ordinal "+" n:int
| o:ordinal "+" n:int
when m <<= Ord F
-> in_pos _loc (ESucc(o,n))
(* Ordinal (parenthesis) *)
@@ -6,7 +6,7 @@ type min⟨n,f⟩ = ∀p, p ∈ nat → leq (f n) (f p)

type bot = ∀x:ο,x

val rec leq_size : ∀o, ∀m∈nat^(o+1), ∀n∈nat, either⟨leq m n, n∈nat^o⟩ =
val rec leq_size : ∀o, ∀m∈nat^(o+ₒ1), ∀n∈nat, either⟨leq m n, n∈nat^o⟩ =
fun m n {
case m {
Zero → case n {
@@ -32,10 +32,10 @@ val rec leq_size : ∀o, ∀m∈nat^(o+1), ∀n∈nat, either⟨leq m n, n∈nat
val rec fn : ∀f∈(nat ⇒ nat), ∀n∈nat, ∀q∈(nat | q ≡ f n),
(∀n∈ nat, min⟨n,f⟩ → bot) → bot =
fun f n q k {
let o such that q : nat^(o+1);
let o such that q : nat^(o+ₒ1);
k (n:nat) (fun p {
let fp = f p;
case leq_size (q:nat^(o+1)) fp {
case leq_size (q:nat^(o+ₒ1)) fp {
InL → {}
InR[fp] → fn f p fp k
}} : min⟨n,f⟩)
@@ -46,7 +46,7 @@ val sbit_average : sbit ⇒ real ⇒ real =
fun d r { cons d r }

// Average function with a carry.
val rec average_aux : ∀s, int ⇒ sreal⟨s+1⟩ ⇒ sreal⟨s+1⟩ ⇒ sreal⟨s⟩ =
val rec average_aux : ∀s, int ⇒ sreal⟨s+ₒ1⟩ ⇒ sreal⟨s+ₒ1⟩ ⇒ sreal⟨s⟩ =
fun carry x y _ {
let {hd = x0; tl = x} = x {};
let {hd = y0; tl = y} = y {};
@@ -7,14 +7,14 @@ type rec rose⟨a⟩ = list⟨rose⟩

val rec size : ∀a, rose⟨a⟩ ⇒ nat =
fun l {
let o,a such that l : rose^(o+1)⟨a⟩;
let o,a such that l : rose^(o+ₒ1)⟨a⟩;
let fn : nat ⇒ rose^(o)⟨a⟩ ⇒ nat = fun acc e { acc + (size e) };
fold_left fn 1 (l:list⟨rose^o⟨a⟩⟩)
}

val rec height : ∀a, rose⟨a⟩ ⇒ nat =
fun l {
let o,a such that l : rose^(o+1)⟨a⟩;
let o,a such that l : rose^(o+ₒ1)⟨a⟩;
let fn : nat ⇒ rose^(o)⟨a⟩ ⇒ nat = fun acc e { max acc S[height e] };
fold_left fn 0 (l:list⟨rose^o⟨a⟩⟩)
}
@@ -31,7 +31,7 @@ val rec map : ∀o, ∀a b, (a ⇒ b) ⇒ stream^o⟨a⟩ ⇒ stream^o⟨b⟩ =
}


val cons : ∀o, ∀a, a ⇒ stream^o⟨a⟩ ⇒ stream^(o+1)⟨a⟩ =
val cons : ∀o, ∀a, a ⇒ stream^o⟨a⟩ ⇒ stream^(o+ₒ1)⟨a⟩ =
fun a s _ {
{ hd = a; tl = s }
}

0 comments on commit 34b595e

Please sign in to comment.
You can’t perform that action at this time.