| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Real_Time_Deque/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 971 B |
|
Quelle Stack.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
section ‹Stack› theory Stack imports Type_Classes begin text ‹A datatype encapsulating two lists. Is used as a base data-structure in dif has the operations ‹push›, ‹pop› and ‹first›. datatype (plugins del: size) 'a stack = Stack "'a list" "'a list" fun push :: "'a → 'a stack → 'a stack" where "push x (Stack left right) = Stack (x#left) right" fun pop :: "'a stack → 'a stack" where "pop (Stack [] []) = Stack [] []" | "pop (Stack (x#left) right) = Stack left right" | "pop (Stack [] (x#right)) = Stack [] right" fun first :: "'a stack → 'a" where "first (Stack (x#left) right) = x" | "first (Stack [] (x#right)) = x" instantiation stack ::(type) is_empty begin fun is_empty_stack where "is_empty_stack (Stack [] []) = True" | "is_empty_stack _ = False" instance.. end end
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01