mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 11:30:30 +03:00
fix unchecked let
This commit is contained in:
parent
b489c148bf
commit
981b8afe90
@ -1,7 +1,7 @@
|
|||||||
Bool.match
|
Bool.match
|
||||||
: ∀(b: Bool)
|
(b: Bool)
|
||||||
∀(P: ∀(x: Bool) *)
|
(P: ∀(x: Bool) *)
|
||||||
∀(t: (P Bool.true))
|
(t: (P Bool.true))
|
||||||
∀(f: (P Bool.false))
|
(f: (P Bool.false))
|
||||||
(P b)
|
: (P b)
|
||||||
= λb λP λt λf (~b P t f)
|
= (~b P t f)
|
||||||
|
@ -1,3 +1,2 @@
|
|||||||
Char.equal
|
Char.equal (a: Char) (b: Char) : Bool =
|
||||||
: ∀(a: Char) ∀(b: Char) Bool
|
(U60.equal a b)
|
||||||
= U60.equal
|
|
||||||
|
@ -1,43 +1,14 @@
|
|||||||
Char.escapes
|
Char.escapes
|
||||||
: (List (Pair Char Char))
|
: (List (Pair Char Char))
|
||||||
= (List.cons
|
= [
|
||||||
(Pair Char Char)
|
(Pair.new _ _ #98 #8)
|
||||||
(Pair.new Char Char #98 #8)
|
(Pair.new _ _ #102 #12)
|
||||||
(List.cons
|
(Pair.new _ _ #110 #10)
|
||||||
(Pair Char Char)
|
(Pair.new _ _ #114 #13)
|
||||||
(Pair.new Char Char #102 #12)
|
(Pair.new _ _ #116 #9)
|
||||||
(List.cons
|
(Pair.new _ _ #118 #11)
|
||||||
(Pair Char Char)
|
(Pair.new _ _ #92 #92)
|
||||||
(Pair.new Char Char #110 #10)
|
(Pair.new _ _ #34 #34)
|
||||||
(List.cons
|
(Pair.new _ _ #48 #0)
|
||||||
(Pair Char Char)
|
(Pair.new _ _ #39 #39)
|
||||||
(Pair.new Char Char #114 #13)
|
]
|
||||||
(List.cons
|
|
||||||
(Pair Char Char)
|
|
||||||
(Pair.new Char Char #116 #9)
|
|
||||||
(List.cons
|
|
||||||
(Pair Char Char)
|
|
||||||
(Pair.new Char Char #118 #11)
|
|
||||||
(List.cons
|
|
||||||
(Pair Char Char)
|
|
||||||
(Pair.new Char Char #92 #92)
|
|
||||||
(List.cons
|
|
||||||
(Pair Char Char)
|
|
||||||
(Pair.new Char Char #34 #34)
|
|
||||||
(List.cons
|
|
||||||
(Pair Char Char)
|
|
||||||
(Pair.new Char Char #48 #0)
|
|
||||||
(List.cons
|
|
||||||
(Pair Char Char)
|
|
||||||
(Pair.new Char Char #39 #39)
|
|
||||||
(List.nil (Pair Char Char))
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
)
|
|
||||||
|
@ -1,7 +1,5 @@
|
|||||||
Char.is_between
|
Char.is_between (min: Char) (max: Char) (chr: Char) : Bool
|
||||||
: ∀(min: Char) ∀(max: Char) ∀(chr: Char) Bool
|
= (Bool.and
|
||||||
= λmin λmax λchr
|
|
||||||
(Bool.and
|
|
||||||
(U60.to_bool #(>= chr min))
|
(U60.to_bool #(>= chr min))
|
||||||
(U60.to_bool #(<= chr max))
|
(U60.to_bool #(<= chr max))
|
||||||
)
|
)
|
@ -1,3 +1,2 @@
|
|||||||
Char.is_blank
|
Char.is_blank (a: Char) : Bool =
|
||||||
: ∀(a: Char) Bool
|
(Bool.or (Char.equal a #10) (Char.equal a #32))
|
||||||
= λa (Bool.or (Char.equal a #10) (Char.equal a #32))
|
|
||||||
|
@ -1,3 +1,2 @@
|
|||||||
Char.is_decimal
|
Char.is_decimal (a: Char) : Bool =
|
||||||
: ∀(a: Char) Bool
|
(Char.is_between #48 #57 a)
|
||||||
= λa (Char.is_between #48 #57 a)
|
|
||||||
|
@ -17,3 +17,5 @@ Char.is_name
|
|||||||
)
|
)
|
||||||
)
|
)
|
||||||
)
|
)
|
||||||
|
|
||||||
|
|
||||||
|
@ -2,19 +2,23 @@
|
|||||||
//| cons (len: Nat) (head: A) (tail: (Vector A len)) : (Vector A (Nat.succ len))
|
//| cons (len: Nat) (head: A) (tail: (Vector A len)) : (Vector A (Nat.succ len))
|
||||||
//| nil : (Vector A Nat.zero)
|
//| nil : (Vector A Nat.zero)
|
||||||
|
|
||||||
use Nat.{succ,zero}
|
//use Nat.{succ,zero}
|
||||||
|
|
||||||
_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
|
_main : Nat =
|
||||||
match a {
|
(Nat.add 1 2)
|
||||||
succ: match b {
|
|
||||||
succ: e
|
|
||||||
zero: e
|
//_main (a: Nat) (b: Nat) (e: (Equal A a b)) : (Equal A a b) =
|
||||||
}
|
//match a {
|
||||||
zero: match b {
|
//succ: match b {
|
||||||
succ: e
|
//succ: e
|
||||||
zero: ?D
|
//zero: e
|
||||||
}
|
//}
|
||||||
}
|
//zero: match b {
|
||||||
|
//succ: e
|
||||||
|
//zero: ?D
|
||||||
|
//}
|
||||||
|
//}
|
||||||
|
|
||||||
//λa λb λe
|
//λa λb λe
|
||||||
//use a.P = _
|
//use a.P = _
|
||||||
|
@ -655,8 +655,8 @@ termCheckGo src (Hol termNam termCtx) typx dep = do
|
|||||||
termCheckGo src (Met uid spn) typx dep = do
|
termCheckGo src (Met uid spn) typx dep = do
|
||||||
return ()
|
return ()
|
||||||
termCheckGo src (Ann chk val typ) typx dep = do
|
termCheckGo src (Ann chk val typ) typx dep = do
|
||||||
if chk then do
|
|
||||||
termCheckCompare src val typ typx dep
|
termCheckCompare src val typ typx dep
|
||||||
|
if chk then do
|
||||||
termCheck src val typ dep
|
termCheck src val typ dep
|
||||||
else do
|
else do
|
||||||
return ()
|
return ()
|
||||||
|
@ -1,6 +1,5 @@
|
|||||||
use crate::{*};
|
use crate::{*};
|
||||||
|
|
||||||
|
|
||||||
impl<'i> KindParser<'i> {
|
impl<'i> KindParser<'i> {
|
||||||
|
|
||||||
pub fn parse_oper(&mut self) -> Result<Oper, String> {
|
pub fn parse_oper(&mut self) -> Result<Oper, String> {
|
||||||
@ -76,9 +75,9 @@ impl<'i> KindParser<'i> {
|
|||||||
val: Box::new(Term::App {
|
val: Box::new(Term::App {
|
||||||
fun: Box::new(Term::App {
|
fun: Box::new(Term::App {
|
||||||
fun: Box::new(Term::Var { nam: "Equal.refl".to_string() }),
|
fun: Box::new(Term::Var { nam: "Equal.refl".to_string() }),
|
||||||
arg: Box::new(Term::Met {})
|
arg: Box::new(Term::Met {}),
|
||||||
}),
|
}),
|
||||||
arg: Box::new(Term::Met {})
|
arg: Box::new(Term::Met {}),
|
||||||
})
|
})
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user