style tweaks
This commit is contained in:
parent
0c1b3a78c3
commit
28eb99c091
3 changed files with 40 additions and 42 deletions
|
|
@ -13,22 +13,20 @@ record AnyTerm where
|
|||
public export
|
||||
record Definition where
|
||||
constructor MkDef'
|
||||
qty : Qty
|
||||
0 qtyGlobal : IsGlobal qty
|
||||
type : AnyTerm
|
||||
term : Maybe AnyTerm
|
||||
qty : Qty
|
||||
type : AnyTerm
|
||||
term : Maybe AnyTerm
|
||||
{auto 0 qtyGlobal : IsGlobal qty}
|
||||
|
||||
public export %inline
|
||||
MkDef : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
|
||||
(type, term : forall d, n. Term d n) -> Definition
|
||||
MkDef {qty, type, term} =
|
||||
MkDef' {qty, qtyGlobal = %search, type = T type, term = Just (T term)}
|
||||
mkDef : (qty : Qty) -> (0 _ : IsGlobal qty) =>
|
||||
(type, term : forall d, n. Term d n) -> Definition
|
||||
mkDef qty type term = MkDef' {qty, type = T type, term = Just (T term)}
|
||||
|
||||
public export %inline
|
||||
MkAbstract : (qty : Qty) -> (0 qtyGlobal : IsGlobal qty) =>
|
||||
mkAbstract : (qty : Qty) -> (0 _ : IsGlobal qty) =>
|
||||
(type : forall d, n. Term d n) -> Definition
|
||||
MkAbstract {qty, type} =
|
||||
MkDef' {qty, qtyGlobal = %search, type = T type, term = Nothing}
|
||||
mkAbstract qty type = MkDef' {qty, type = T type, term = Nothing}
|
||||
|
||||
|
||||
public export %inline
|
||||
|
|
|
|||
|
|
@ -202,11 +202,11 @@ mutual
|
|||
isRedexT (E e@(_ :@ _)) with (isRedexE e)
|
||||
_ | Yes yes = Yes $ IsERedex yes
|
||||
_ | No no = No \case IsERedex p => no p
|
||||
isRedexT (TYPE {}) = No $ \x => case x of {}
|
||||
isRedexT (Pi {}) = No $ \x => case x of {}
|
||||
isRedexT (Lam {}) = No $ \x => case x of {}
|
||||
isRedexT (E (F _)) = No $ \x => case x of IsERedex _ impossible
|
||||
isRedexT (E (B _)) = No $ \x => case x of IsERedex _ impossible
|
||||
isRedexT (TYPE {}) = No $ \case _ impossible
|
||||
isRedexT (Pi {}) = No $ \case _ impossible
|
||||
isRedexT (Lam {}) = No $ \case _ impossible
|
||||
isRedexT (E (F _)) = No $ \case IsERedex _ impossible
|
||||
isRedexT (E (B _)) = No $ \case IsERedex _ impossible
|
||||
|
||||
export %inline
|
||||
isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
|
||||
|
|
@ -214,28 +214,28 @@ mutual
|
|||
isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam
|
||||
isRedexE (CloE {}) = Yes IsCloE
|
||||
isRedexE (DCloE {}) = Yes IsDCloE
|
||||
isRedexE (F x) = No $ \x => case x of {}
|
||||
isRedexE (B i) = No $ \x => case x of {}
|
||||
isRedexE (F _ :@ _) = No $ \x => case x of {}
|
||||
isRedexE (B _ :@ _) = No $ \x => case x of {}
|
||||
isRedexE (_ :@ _ :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((TYPE _ :# _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((Pi {} :# _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((Lam {} :# TYPE _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((Lam {} :# Lam {}) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((Lam {} :# E _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((Lam {} :# CloT {}) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((Lam {} :# DCloT {}) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((E _ :# _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((CloT {} :# _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE ((DCloT {} :# _) :@ _) = No $ \x => case x of {}
|
||||
isRedexE (CloE {} :@ _) = No $ \x => case x of {}
|
||||
isRedexE (DCloE {} :@ _) = No $ \x => case x of {}
|
||||
isRedexE (TYPE _ :# _) = No $ \x => case x of {}
|
||||
isRedexE (Pi {} :# _) = No $ \x => case x of {}
|
||||
isRedexE (Lam {} :# _) = No $ \x => case x of {}
|
||||
isRedexE (CloT {} :# _) = No $ \x => case x of {}
|
||||
isRedexE (DCloT {} :# _) = No $ \x => case x of {}
|
||||
isRedexE (F x) = No $ \case _ impossible
|
||||
isRedexE (B i) = No $ \case _ impossible
|
||||
isRedexE (F _ :@ _) = No $ \case _ impossible
|
||||
isRedexE (B _ :@ _) = No $ \case _ impossible
|
||||
isRedexE (_ :@ _ :@ _) = No $ \case _ impossible
|
||||
isRedexE ((TYPE _ :# _) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((Pi {} :# _) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((Lam {} :# TYPE _) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((Lam {} :# Lam {}) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((Lam {} :# E _) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((Lam {} :# CloT {}) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((Lam {} :# DCloT {}) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((E _ :# _) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((CloT {} :# _) :@ _) = No $ \case _ impossible
|
||||
isRedexE ((DCloT {} :# _) :@ _) = No $ \case _ impossible
|
||||
isRedexE (CloE {} :@ _) = No $ \case _ impossible
|
||||
isRedexE (DCloE {} :@ _) = No $ \case _ impossible
|
||||
isRedexE (TYPE _ :# _) = No $ \case _ impossible
|
||||
isRedexE (Pi {} :# _) = No $ \case _ impossible
|
||||
isRedexE (Lam {} :# _) = No $ \case _ impossible
|
||||
isRedexE (CloT {} :# _) = No $ \case _ impossible
|
||||
isRedexE (DCloT {} :# _) = No $ \case _ impossible
|
||||
|
||||
|
||||
public export %inline
|
||||
|
|
|
|||
|
|
@ -161,11 +161,11 @@ tests = "equality & subtyping" :- [
|
|||
|
||||
"free var" :-
|
||||
let au_bu = fromList
|
||||
[("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
|
||||
("B", MkDef Any (TYPE (U 1)) (TYPE (U 0)))]
|
||||
[("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
|
||||
("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))]
|
||||
au_ba = fromList
|
||||
[("A", MkDef Any (TYPE (U 1)) (TYPE (U 0))),
|
||||
("B", MkDef Any (TYPE (U 1)) (FT "A"))]
|
||||
[("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))),
|
||||
("B", mkDef Any (TYPE (U 1)) (FT "A"))]
|
||||
in [
|
||||
testEq "A ≡ A" $
|
||||
equalE (F "A") (F "A"),
|
||||
|
|
|
|||
Loading…
Reference in a new issue