Skip to main content

Browse the archive

https://github.com/jaycech3n/Isabelle-HoTT
07 June 2021, 00:05:13 UTC
Revision 00463d770fd738749c092829e3b49e4f7d25f75e authored by Josh Chen on 17 July 2020, 09:12:00 UTC, committed by Josh Chen on 17 July 2020, 09:12:00 UTC 
looks like descriptions not allowed in workflow job yaml
1 parent 9eb4aeb
Raw File
Tip revision: 00463d770fd738749c092829e3b49e4f7d25f75e authored by Josh Chen on 17 July 2020, 09:12:00 UTC
looks like descriptions not allowed in workflow job yaml
Tip revision: 00463d7
More_List.thy 
theory More_List
imports
  Spartan.List
  Nat

begin

section \<open>Length\<close>

definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)"

experiment begin
  Lemma "len [] \<equiv> ?n" by (subst comps)+
  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
end


end
back to top