Fixes.

parent e713a9cc
......@@ -15,28 +15,29 @@ theory NatExample : ?LFI =


theory TestExample : ?LFI =
m : type ❙
bla : type ❙
// theory TestExample : ?LFI =
// m : type ❙
// bla : type ❙
inductive stressTest(R: type) ❘ =
a: type ❙
r : type ❙
b: {x:a} type ❙
c: {x:a, y: b x} type ❘ # 1 ° 2 ❙
// This currently works, but is problematic when inductive types are elaborated to defined derived declarations ❙
d: bla ⟶ r ⟶ bla ❙
e: r ⟶ bla ⟶ r ❘ # 1 e 2 ❙
f: bla ⟶ r ❙
k: bla ❙
l: {x:a} b x ❙
m: {x:a, y: b x} c x y ❙
n: {x:a} a ❙
o: {x:a, y: b x} c x y ⟶ a ❙
p: {x:a, y: b x} b x ⟶ c x y ❙
q: {x:a} a ⟶ b x ❙


// inductive stressTest(R: type) ❘ =
// a: type ❙
// r : type ❙
// b: {x:a} type ❙
// c: {x:a, y: b x} type ❘ # 1 ° 2 ❙
// // This currently works, but is problematic when inductive types are elaborated to defined derived declarations ❙
// d: bla ⟶ r ⟶ bla ❙
// e: r ⟶ bla ⟶ r ❘ # 1 e 2 ❙
// f: bla ⟶ r ❙
// k: bla ❙
// l: {x:a} b x ❙
// m: {x:a, y: b x} c x y ❙
// n: {x:a} a ❙
// o: {x:a, y: b x} c x y ⟶ a ❙
// p: {x:a, y: b x} b x ⟶ c x y ❙
// q: {x:a} a ⟶ b x ❙
// 
// ❚
theory InductivelyDefinedTypes : ?LFI =
inductive nat()❘=
......@@ -44,49 +45,49 @@ theory InductivelyDefinedTypes : ?LFI =
z: n
s: n ⟶ n

plus: nat/n → nat/n → nat/n ❘ = [m, n] ((nat/induct n (nat/n → nat/n) ([x] x) [u] ([x] nat/s (u x))) m) n ❙
times: nat/n → nat/n → nat/n ❘ = plus: nat/n → nat/n → nat/n ❘ = [m, n] ((nat/induct n (nat/n → nat/n) ([x] ❘) [u] ([x] nat/s (u ❘))) m) n ❙
plus: nat/n ⟶ nat/n ⟶ nat/n ❘= [m, n] ((nat/induct_n (nat/n ⟶ nat/n) ([x] x) ([u] ([x] nat/s (u x)))) m) n ❙
times: nat/n ⟶ nat/n ⟶ nat/n ❘= [m, n] ((nat/induct_n (nat/n ⟶ nat/n) ([x] nat/z) ([u] ([x] nat/s (u x)))) m) n ❙
inductive list(a : type) ❘ =
list: type ❙
nil: list a ❙
cons: a → list a → list a ❙
concat: {a : type} list/list a → list/list a ❘ = [a, l, m] (list/induct_list ((list/list a → list/list a) ([tp, ys] ys) [tp, x, xs] ([l] list_cons t x (l ys))) l) m ❙
single: {a : type} a → list/list a ❘ = [a : type, x : a] list/cons x list/nil
reverse:{a: type} list/list a → list/list a ❘ = [a, l] list/induct_list a (list/list a) ([tp] list/nil tp) [tp, x, xs] concat tp (reverse xs) (single x) ❙
length: {a : type} list/list a → nat/nat ❘ = [a, l] list/induct_list a nat/n ([tp] nat/z) [tp, x, xs] nat/s (length xs) ❙
inductive list1() ❘ =
list:{a:type} type 
nil:{a:type} list a 
cons:{a:type} a ⟶ list a ⟶ list a

concat: {a : type} list1/list a ⟶ list1/list a ❘ = [a, l, m] (list1/induct_list ((list1/list a ⟶ list1/list a) ([tp, ys] ys) ([tp, x, xs] ([l] list1/cons a x (l xs)))) l) m ❙
single: {a : type} a ⟶ list1/list a ❘ = [a, x] list1/cons a x (list1/nil a)
reverse: {a: type} list1/list a ⟶ list1/list a ❘ = [a, l] list1/induct_list a (list1/list a) ([tp] list1/nil tp) [tp, x, xs] concat tp (reverse xs) (single x) ❙
length: {a : type} list1/list a ⟶ nat/n ❘ = [a, l] list1/induct_list a nat/n ([tp] nat/z) [tp, x, xs] nat/s (length xs) ❙
inductive vector(a: type, n: nat/n) ❘ =
vec: {n: nat/n} type ❙
empty: vec a nat/z ❙
add: {n: nat/n} vec a n → a → vec a (nat/s n) ❙
empty: vec nat/z ❙
add: {n: nat/n} vec n ⟶ a ⟶ vec (nat/s n) ❙

zip: {a: type, b: type, n: nat/n} vec a n → vec b n → vec (a * b) n ❘ = [a, b, n, l, m] ((vector/induct_vec (a*b)) ([l:vector/vec a n, len: nat/n] vec (a*b) n) ([l: vec a n] ([m: vec b n] vector/empty (a*b))) ([l: vec a n] ([len: nat/n, tlm: vec b n, hdm: b] (vector/induct_vec (a*b) ([lenl: nat/n] vec (a*b) lenl) (vector/empty (a*b)) ([lenl: nat/n, tll: vec a lenl, hdl: a] vector/add a n (zip a b n tll tlm) (hdl, hdm))) l)) l) m ❙
zip: {a: type, b: type, n: nat/n} vector/vec a n ⟶ vector/vec b n ⟶ vector/vec (a * b) n ❘ = [a, b, n, l, m] ((vector/induct_vec (a*b)) ([l:vector/vec a n, len: nat/n] vector/vec (a*b) n) ([l: vector/vec a n] ([m: vector/vec b n] vector/empty (a*b))) ([l: vector/vec a n] ([len: nat/n, tlm: vector/vec b n, hdm: b] (vector/induct_vec (a*b) ([lenl: nat/n] vector/vec (a*b) lenl) (vector/empty (a*b)) ([lenl: nat/n, tll: vector/vec a lenl, hdl: a] vector/add a n (zip a b n tll tlm) (hdl, hdm))) l)) l) m ❙
inductive_list2() ❘ =
list: type type ❙
list: type type ❙
nil: {a: type} list2 a ❙
cons: {a: type} a → list a → list a ❙
length: {a} list a nat/n ❙
cons: {a: type} a ⟶ list a ⟶ list a ❙
length: {a} list a nat/n ❙
length_nil: {a: type} length (nil a) ≐ nat/z ❙
length_cons: {a:type, hd: a, tl: list a} length a (cons a hd l) ≐ nat/s (length a tl) (nat/s nat/z) ❙
inductive list3() ❘ =
list: type type ❙
list: type type ❙
nil: {a : type} list a ❙
cons: {a : type} a → list a → list a ❙
head: {a : type, l:list a} → ⊦ l ≐ nil a → a
cons: {a : type} a ⟶ list a ⟶ list a ❙
head: {a : type, l:list a} ⟶ ⊦ l ≐ nil a ⟶ a ❙
head_cons: {a: type, hd: a, tl: list a, P: ⊦ l ≐ nil} ⊦ head a (cons a hd tl) P ≐ hd ❙
induct freeMonoid(a: type) ❘ =
fm: type ❙
gen: a fm ❙
gen: a fm ❙
unit: fm ❙
comp: fm → fm → fm ❘ # 1 . 2 ❙
comp: fm ⟶ fm ⟶ fm ❘ # 1 . 2 ❙
assoc: {x: fm, y: fm, z: fm} ⊦ (x . y) . z ≐ x . (y . z) ❙
unit_r: {x: fm} ⊦ x . unit ≐ x❙
unit_l: {x: fm} ⊦ unit . x ≐ 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