Last active
October 12, 2022 21:01
-
-
Save jfdm/8f40e7a65aa5e854c3cb8542b0163960 to your computer and use it in GitHub Desktop.
Indexing terms with versioning.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
λΠ> :t Deprecated.L (N 2) (L (N 1) (B False)) | |
L (N 2) (L (N 1) (B False)) : Term ?ctxt (Just 1) TyNat | |
λΠ> :t L (S "w") (L (N 1) (B False)) | |
L (S "w") (L (N 1) (B False)) : Term ?ctxt Nothing TyNat | |
λΠ> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Versioned | |
import Data.List.Elem | |
import Data.List.Quantifiers | |
import Data.Nat | |
%default total | |
data Ty | |
= TyNat | |
| TyBool | |
| TyString | |
namespace Simple | |
public export | |
data Term : List (Nat, Ty) -> Nat -> Ty -> Type | |
where | |
N : Nat -> Term ctxt 0 TyNat | |
B : Bool -> Term ctxt 1 TyNat | |
V : Elem (v,type) ctxt -> Term ctxt v type | |
L : Term ctxt v a | |
-> Term (MkPair v a::ctxt) w b | |
-> Term ctxt (max v w) b | |
namespace Deprecated | |
public export | |
cmp : (a,b : Maybe Nat) -> Maybe Nat | |
cmp a b = max <$> a <*> b | |
public export | |
data Term : List (Maybe Nat, Ty) -> Maybe Nat -> Ty -> Type | |
where | |
D : Term ctxt v type | |
-> Term ctxt Nothing type | |
S : String -> Term ctxt (Just 1) TyString | |
N : Nat -> Term ctxt (Just 0) TyNat | |
B : Bool -> Term ctxt (Just 1) TyNat | |
V : Elem (v,type) ctxt -> Term ctxt v type | |
L : Term ctxt v a | |
-> Term (MkPair v a::ctxt) w b | |
-> Term ctxt (cmp v w) b |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment