Commit 2023-03-25 13:19 66aed115

View on Github →

feat: port/Computability.Primrec (#2360)

Estimated changes

added def Nat.Primrec'.Vec
added theorem Nat.Primrec'.add
added theorem Nat.Primrec'.comp'
added theorem Nat.Primrec'.comp₁
added theorem Nat.Primrec'.comp₂
added theorem Nat.Primrec'.const
added theorem Nat.Primrec'.head
added theorem Nat.Primrec'.idv
added theorem Nat.Primrec'.if_lt
added theorem Nat.Primrec'.mkpair
added theorem Nat.Primrec'.mul
added theorem Nat.Primrec'.of_eq
added theorem Nat.Primrec'.of_prim
added theorem Nat.Primrec'.prec'
added theorem Nat.Primrec'.pred
added theorem Nat.Primrec'.prim_iff
added theorem Nat.Primrec'.sqrt
added theorem Nat.Primrec'.sub
added theorem Nat.Primrec'.tail
added theorem Nat.Primrec'.to_prim
added theorem Nat.Primrec'.unpair₁
added theorem Nat.Primrec'.unpair₂
added theorem Nat.Primrec'.vec_iff
added inductive Nat.Primrec'
added theorem Nat.Primrec.add
added theorem Nat.Primrec.cases1
added theorem Nat.Primrec.cases
added theorem Nat.Primrec.const
added theorem Nat.Primrec.mul
added theorem Nat.Primrec.of_eq
added theorem Nat.Primrec.pow
added theorem Nat.Primrec.prec1
added theorem Nat.Primrec.pred
added theorem Nat.Primrec.sub
added theorem Nat.Primrec.swap'
added def Nat.unpaired
added theorem Primrec.comp
added theorem Primrec.comp₂
added theorem Primrec.cond
added theorem Primrec.const
added theorem Primrec.dom_bool
added theorem Primrec.dom_bool₂
added theorem Primrec.dom_fintype
added theorem Primrec.encdec
added theorem Primrec.encode_iff
added theorem Primrec.fin_app
added theorem Primrec.fin_curry
added theorem Primrec.fin_curry₁
added theorem Primrec.fin_succ
added theorem Primrec.fin_val
added theorem Primrec.fin_val_iff
added theorem Primrec.fst
added theorem Primrec.ite
added theorem Primrec.list_append
added theorem Primrec.list_cases
added theorem Primrec.list_concat
added theorem Primrec.list_cons
added theorem Primrec.list_findIdx
added theorem Primrec.list_foldl
added theorem Primrec.list_foldr
added theorem Primrec.list_get?
added theorem Primrec.list_get?₁
added theorem Primrec.list_getD
added theorem Primrec.list_getI
added theorem Primrec.list_head?
added theorem Primrec.list_headI
added theorem Primrec.list_indexOf
added theorem Primrec.list_join
added theorem Primrec.list_length
added theorem Primrec.list_map
added theorem Primrec.list_ofFn
added theorem Primrec.list_range
added theorem Primrec.list_rec
added theorem Primrec.list_reverse
added theorem Primrec.list_tail
added theorem Primrec.map_decode_iff
added theorem Primrec.nat_add
added theorem Primrec.nat_bodd
added theorem Primrec.nat_cases'
added theorem Primrec.nat_cases
added theorem Primrec.nat_cases₁
added theorem Primrec.nat_div2
added theorem Primrec.nat_div
added theorem Primrec.nat_double
added theorem Primrec.nat_elim'
added theorem Primrec.nat_elim
added theorem Primrec.nat_elim₁
added theorem Primrec.nat_iff
added theorem Primrec.nat_iterate
added theorem Primrec.nat_le
added theorem Primrec.nat_lt
added theorem Primrec.nat_max
added theorem Primrec.nat_min
added theorem Primrec.nat_mod
added theorem Primrec.nat_mul
added theorem Primrec.nat_sqrt
added theorem Primrec.nat_strong_rec
added theorem Primrec.nat_sub
added theorem Primrec.ofEquiv
added theorem Primrec.ofEquiv_iff
added theorem Primrec.ofEquiv_symm
added theorem Primrec.ofNat_iff
added theorem Primrec.of_eq
added theorem Primrec.of_graph
added theorem Primrec.option_bind
added theorem Primrec.option_bind₁
added theorem Primrec.option_cases
added theorem Primrec.option_get
added theorem Primrec.option_getD
added theorem Primrec.option_guard
added theorem Primrec.option_iget
added theorem Primrec.option_isSome
added theorem Primrec.option_map
added theorem Primrec.option_map₁
added theorem Primrec.option_orElse
added theorem Primrec.option_some
added theorem Primrec.pair
added theorem Primrec.pred
added theorem Primrec.snd
added theorem Primrec.subtype_mk
added theorem Primrec.subtype_val
added theorem Primrec.succ
added theorem Primrec.sum_cases
added theorem Primrec.sum_inl
added theorem Primrec.sum_inr
added theorem Primrec.to₂
added theorem Primrec.ulower_down
added theorem Primrec.ulower_up
added theorem Primrec.unpair
added theorem Primrec.vector_cons
added theorem Primrec.vector_get
added theorem Primrec.vector_head
added theorem Primrec.vector_length
added theorem Primrec.vector_nth'
added theorem Primrec.vector_ofFn
added theorem Primrec.vector_of_fn'
added theorem Primrec.vector_tail
added theorem Primrec.vector_toList
added def Primrec
added theorem PrimrecPred.and
added theorem PrimrecPred.comp
added theorem PrimrecPred.not
added theorem PrimrecPred.of_eq
added theorem PrimrecPred.or
added def PrimrecPred
added theorem PrimrecRel.comp
added theorem PrimrecRel.comp₂
added theorem PrimrecRel.of_eq
added def PrimrecRel
added theorem Primrec₂.comp
added theorem Primrec₂.comp₂
added theorem Primrec₂.const
added theorem Primrec₂.curry
added theorem Primrec₂.encode_iff
added theorem Primrec₂.left
added theorem Primrec₂.mkpair
added theorem Primrec₂.nat_iff'
added theorem Primrec₂.nat_iff
added theorem Primrec₂.ofNat_iff
added theorem Primrec₂.of_eq
added theorem Primrec₂.right
added theorem Primrec₂.swap
added theorem Primrec₂.uncurry
added theorem Primrec₂.unpaired'
added theorem Primrec₂.unpaired
added def Primrec₂
added theorem List.findIdx_cons
added theorem List.findIdx_nil