--#include "Lib/Op/Fin.alfa" open SET use Absurd, Unit, Nat, Vec, Bool, List, Plus, Times, fst, snd, pair, Fin open OpBool use and open OpNat use zero, one, two, unit, succ, pred, (+), (*), (^), (==), (<=), (<), absdiff, max, min open OpFin use PreMon, tail, prodM, filterM, sum, prod, exist, forall, count_sub, count_qout compose (A::Set)(B::Set)(C::Set)(f::B -> C)(g::A -> B) :: A -> C = \(x::A) -> f (g x) elimFinZero (A::Set)(h::Fin zer@_) :: A = case h of { } FVec (n::Nat)(A::Set) :: Set = Fin n -> A fnil (A::Set) :: FVec zer@_ A = elimFinZero A fcons (n::Nat)(A::Set)(x::A)(xs::FVec n A) :: FVec (suc@_ n) A = \(h::Fin (suc@_ n)) -> case h of { (zer) -> x; (suc h') -> xs h';} Arity :: Set = Nat Sig :: Set = List Arity Fa (n::Arity)(X::Set) :: Set = Fin n -> X F (fi::Sig)(X::Set) :: Set = case fi of { (nil) -> Absurd; (con n fi') -> Plus (Fa n X) (F fi' X);} Fa1 (n::Arity)(a::Set)(b::Set)(f::a -> b)(x::Fa n a) :: Fa n b = compose (Fin n) a b f x F1 (fi::Sig)(a::Set)(b::Set)(f::a -> b)(x::F fi a) :: F fi b = case fi of { (nil) -> case x of { }; (con x' xs) -> case x of { (inl x0) -> inl@_ (compose (Fin x') a b f x0); (inr y) -> inr@_ (F1 xs a b f y);};} T (fi::Sig) :: Set = data Intro (i::F fi (T fi)) It (fi::Sig)(C::Set)(d::F fi C -> C) :: T fi -> C = \(h::T fi) -> case h of { (Intro i) -> d (F1 fi (T fi) C (It fi C d) i);} MIt (fi::Sig)(C::Set)(s::(X::Set) -> (X -> C) -> F fi X -> C)(x::T fi) :: C = case x of { (Intro i) -> s (T fi) (MIt fi C s) i;} size_step (fi::Sig)(x::F fi Nat) :: Nat = case fi of { (nil) -> case x of { }; (con n ns) -> case x of { (inl x0) -> unit + (sum n x0); (inr x1) -> size_step ns x1;};} size (fi::Sig) :: T fi -> Nat = It fi Nat (size_step fi) eq_step' (fi::Sig)(Y::Set)(fs::F fi (Y -> Bool))(h::F fi Y) :: Bool = case fi of { (nil) -> case fs of { }; (con n fi') -> case fs of { (inl f) -> case h of { (inl x) -> forall n (\(h::SET.Fin n) -> f h (x h)); (inr y) -> false@_;}; (inr x) -> case h of { (inl x') -> false@_; (inr y) -> eq_step' fi' Y x y;};};} eq_step (fi::Sig)(fs::F fi (T fi -> Bool)) :: T fi -> Bool = \(h::T fi) -> case h of { (Intro i) -> eq_step' fi (T fi) fs i;} eq (fi::Sig) :: (h::T fi) -> (h'::T fi) -> Bool = It fi (T fi -> Bool) (eq_step fi) codeNat :: Sig = con@_ zer@_ (con@_ (suc@_ zer@_) nil@_) iNat :: Set = T codeNat eqIN :: iNat -> iNat -> Bool = eq codeNat izero :: iNat = Intro@_ (inl@_ (fnil (T codeNat))) isucc :: iNat -> iNat = \(h::iNat) -> Intro@_ (inr@_ (inl@_ (fcons zer@_ (T codeNat) h (fnil (T codeNat))))) ione :: iNat = isucc izero {-# Alfa unfoldgoals off brief on hidetypeannots off wide nd hiding on var "veq" hide 2 var "fi" as "F" with symbolfont var "pair" hide 2 tuple var "fst" hide 2 var "snd" hide 2 var "compose" hide 3 infix as "o" with symbolfont var "fnil" hide 1 var "fcons" hide 2 var "sum" #-}